14

在元编程时,将有关您的程序已知但在 Hindley-Milner 中无法推断的类型的信息传递给 Haskell 的类型系统可能是有用的(或必要的)。在 Haskell 中是否有一个库(或语言扩展等)提供了执行此操作的工具——即编程类型注释?

考虑一种情况,您正在使用异构列表(Data.Dynamic例如,使用库或存在量化实现)并且您希望将列表过滤为沼泽标准、同质类型的 Haskell 列表。你可以写一个函数

import Data.Dynamic
import Data.Typeable

dynListToList :: (Typeable a) => [Dynamic] -> [a]
dynListToList = (map fromJust) . (filter isJust) . (map fromDynamic)

并使用手动类型注释调用它。例如,

foo :: [Int]
foo = dynListToList [ toDyn (1 :: Int)
                    , toDyn (2 :: Int)
                    , toDyn ("foo" :: String) ]

foo是清单[1, 2] :: [Int];这工作得很好,你又回到了 Haskell 的类型系统可以做它的事情的坚实基础上。

现在想象你想做同样的事情,但是(a)在你编写代码时你不知道调用产生的列表的类型dynListToList需要是什么,但是(b)你的程序确实包含弄清楚这一点所需的信息,只有(c)它不是类型系统可以访问的形式。

例如,假设您从异构列表中随机选择了一个项目,并且您希望按类型过滤列表。使用 提供的类型检查工具Data.Typeable,您的程序拥有执行此操作所需的所有信息,但据我所知——这是问题的本质——没有办法将其传递给类型系统。这是一些伪Haskell,说明了我的意思:

import Data.Dynamic
import Data.Typeable

randList :: (Typeable a) => [Dynamic] -> IO [a]
randList dl = do
    tr <- randItem $ map dynTypeRep dl
    return (dynListToList dl :: [<tr>])  -- This thing should have the type
                                         -- represented by `tr`

(假设randItem从列表中选择一个随机项目。)

的参数上没有类型注释return,编译器会告诉你它有一个“不明确的类型”并要求你提供一个。但是您不能提供手动类型注释,因为类型在写入时未知(并且可能会有所不同);然而,该类型在运行时已知的——尽管它是类型系统无法使用的形式(这里,所需的类型由 value tr, a表示TypeRep——Data.Typeable详情请参阅)。

伪代码:: [<tr>]是我想要发生的魔法。有没有办法以编程方式为类型系统提供类型信息?也就是说,程序中的值中包含类型信息?

基本上,我正在寻找一个具有(伪)类型的函数,??? -> TypeRep -> a它采用 Haskell 的类型系统未知的类型的值和 aTypeRep并说:“相信我,编译器,我知道我在做什么。这东西有价值以此为代表TypeRep。” (请注意,这不是什么unsafeCoerce。)

还是有什么完全不同的东西让我在同一个地方?例如,我可以想象一个允许分配给类型变量的语言扩展,例如启用范围类型变量的扩展的增强版本。

(如果这是不可能的或非常不切实际的——例如,它需要将一个完整的类似 GHCi 的解释器打包到可执行文件中——请尝试解释原因。)

4

3 回答 3

18

不,你不能这样做。总而言之,您正在尝试编写依赖类型的函数,而 Haskell 不是依赖类型的语言。你不能将你的TypeRep价值提升到一个真正的类型,所以没有办法写下你想要的函数的类型。为了更详细地解释这一点,我首先要说明为什么你对类型的表述方式randList没有真正意义。然后,我将解释为什么你不能做你想做的事。最后,我将简要提及一些关于实际操作的想法。

存在主义

你的类型签名randList不能代表你想要的意思。记住 Haskell 中的所有类型变量都是普遍量化的,它读取

randList :: forall a. Typeable a => [Dynamic] -> IO [a]

因此,我有权称它为,比如说,randList dyns :: IO [Int]我想要的任何地方;我必须能够为所有人 a提供返回值,而不仅仅是为某些人 a提供。把它想象成一个游戏,它是调用者可以选择a的,而不是函数本身。您想说的(这不是有效的 Haskell 语法,尽管您可以使用存在数据类型1将其转换为有效的 Haskell )更像是

randList :: [Dynamic] -> (exists a. Typeable a => IO [a])

这保证列表的元素是某种类型a的,它是 的一个实例Typeable,但不一定是任何这种类型。但即使这样,你也会遇到两个问题。首先,即使你可以构建这样一个列表,你能用它做什么?其次,事实证明,你甚至不能一开始就构建它。

既然您对存在列表元素的所有了解都是它们是 的实例Typeable,那么您可以用它们做什么呢? 查看文档,我们看到只有两个函数2采用以下实例Typeable

typeOf因此,您对列表中元素类型的所有了解就是您可以调用cast它们。由于我们永远无法对它们有用地做任何其他事情,我们的存在主义也可能是(同样,不是有效的 Haskell)

randList :: [Dynamic] -> IO [(TypeRep, forall b. Typeable b => Maybe b)]

typeOf如果我们对列表的每个元素应用和cast处理,存储结果并丢弃现在无用的存在类型的原始值,这就是我们得到的结果。显然,TypeRep这个列表的一部分没有用。列表的后半部分也不是。由于我们回到了一个普遍量化的类型,调用者randList再次有权请求他们为他们选择的任何(可键入的)获取 a Maybe Int、 aMaybe Bool或 a 。(事实上​​,它们比以前更强大,因为它们可以将列表中的不同元素实例化为不同的类型。)但是除非它们已经知道,否则它们无法确定要转换类型——你仍然知道丢失了您试图保留的类型信息。Maybe bb

即使抛开它们没有用的事实,您也根本无法在这里构造所需的存在类型。当您尝试返回存在类型列表 ( return $ dynListToList dl) 时会出现错误。你打电话的具体类型是什么dynListToList?回想一下dynListToList :: forall a. Typeable a => [Dynamic] -> [a];因此,负责randList挑选要使用的。但它不知道该选哪个;再次,这就是问题的根源!因此,您尝试返回的类型未指定,因此不明确。3 a dynListToLista

依赖类型

好的,那么什么会使这种存在主义有用(并且可能)?好吧,我们实际上有更多的信息:我们不仅知道有一些 a,我们还有它的TypeRep。所以也许我们可以把它打包:

randList :: [Dynamic] -> (exists a. Typeable a => IO (TypeRep,[a]))

但是,这还不够好;theTypeRep和 the[a]根本没有链接。这正是你想要表达的:某种方式来链接TypeRepa

基本上,您的目标是编写类似

toType :: TypeRep -> *

这里,*是所有类型中的那种;如果您以前没有见过种类,那么它们就是类型,什么类型是值。 *对类型* -> *进行分类,对单参数类型构造函数等进行分类(例如,Int :: *Maybe :: * -> *Either :: * -> * -> *Maybe Int :: *.)

有了这个,你可以写(再一次,这段代码不是有效的 Haskell;事实上,它实际上与 Haskell 只是有一点相似,因为你无法在 Haskell 的类型系统中编写它或类似的东西):

randList :: [Dynamic] -> (exists (tr :: TypeRep).
                           Typeable (toType tr) => IO (tr, [toType tr]))
randList dl = do
  tr <- randItem $ map dynTypeRep dl
  return (tr, dynListToList dl :: [toType tr])
    -- In fact, in an ideal world, the `:: [toType tr]` signature would be
    -- inferable.

现在,您承诺了正确的事情:不是存在某种类型对列表的元素进行分类,而是存在某种TypeRep类型使得其对应的类型对​​列表的元素进行分类。如果你能做到这一点,你就会被设置。但是在 Haskell 中编写toType :: TypeRep -> *是完全不可能的:这样做需要依赖类型的语言,因为toType tr它是一种依赖于值的类型。

这是什么意思?在 Haskell 中,值依赖于其他值是完全可以接受的。这就是函数。例如, valuehead "abc"取决于 value "abc"。同样,我们有类型构造函数,因此类型依赖于其他类型是可以接受的;考虑一下Maybe Int,怎么看Int。我们甚至可以拥有取决于类型的值!考虑id :: a -> a。这实际上是一系列函数:id_Int :: Int -> Intid_Bool :: Bool -> Bool等。我们拥有哪一个取决于 的类型a。(真的,id = \(a :: *) (x :: a) -> x; 虽然我们不能在 Haskell 中编写这个,但我们可以使用其他语言。)

然而,至关重要的是,我们永远不能拥有依赖于值的类型。我们可能想要这样一个东西:想象一下Vec 7 Int,长度为 7 的整数列表的类型。这里,Vec :: Nat -> * -> *: 一个类型,其第一个参数必须是 type 的值Nat。但是我们不能在 Haskell 中编写这种东西。4 支持这一点的语言被称为依赖类型id(我们可以像上面那样编写);示例包括CoqAgda。(此类语言通常兼作证明助手,通常用于研究工作而不是编写实际代码。依赖类型很难,使它们对日常编程有用是一个活跃的研究领域。)

因此,在 Haskell 中,我们可以先检查关于类型的所有内容,丢弃所有信息,然后编译仅引用值的内容。事实上,这正是 GHC 所做的;因为在 Haskell 中我们永远无法在运行时检查类型,所以 GHC 在编译时擦除所有类型而不改变程序的运行时行为。这就是为什么unsafeCoerce易于实现(操作上)并且完全不安全的原因:在运行时,它是无操作的,但它取决于类型系统。toType因此,在 Haskell 类型系统中完全不可能实现类似的东西。

事实上,正如您所注意到的,您甚至无法写下所需的类型并使用unsafeCoerce. 对于某些问题,您可以摆脱它;我们可以写下函数的类型,但只能通过作弊来实现。这正是它的fromDynamic工作原理。但正如我们在上面看到的,在 Haskell 中甚至没有一个很好的类型可以解决这个问题。虚toType函数允许你给程序一个类型,但你甚至不能写下toType的类型!

现在怎么办?

所以,你不能这样做。你应该怎么做?我的猜测是您的整体架构对于 Haskell 来说并不理想,尽管我还没有看到它;Typeable并且Dynamic实际上并没有在 Haskell 程序中出现那么多。(正如他们所说,也许您“说的是带有 Python 口音的 Haskell”。)如果您只有一组有限的数据类型要处理,您也许可以将事物捆绑到一个普通的旧代数数据类型中:

data MyType = MTInt Int | MTBool Bool | MTString String

然后您可以编写isMTInt,并且只需使用filter isMTInt, 或filter (isSameMTAs randomMT)

虽然我不知道它是什么,但可能有一种方法可以 unsafeCoerce解决这个问题。但坦率地说,这不是一个好主意,除非你真的、真的、真的、真的、真的、真的知道你在做什么。即便如此,也可能不是。如果你需要unsafeCoerce,你就会知道,这不仅仅是一件方便的事情。

我真的同意Daniel Wagner 的评论:您可能想要从头开始重新考虑您的方法。不过,再一次,因为我还没有看到你的架构,我不能说这意味着什么。如果你能提炼出一个具体的困难,也许那里还有另一个 Stack Overflow 问题。


1如下所示:

{-# LANGUAGE ExistentialQuantification #-}
data TypeableList = forall a. Typeable a => TypeableList [a]
randList :: [Dynamic] -> IO TypeableList

但是,由于无论如何这些代码都没有编译,我认为用它写出来exists更清晰。

2从技术上讲,还有一些看起来相关的其他函数,例如toDyn :: Typeable a => a -> DynamicfromDyn :: Typeable a => Dynamic -> a -> a。但是,Dynamic它或多或少是 s 的存在包装器Typeable,依赖于typeOfand TypeReps 知道何时执行unsafeCoerce(GHC 使用一些特定于实现的类型 and unsafeCoerce,但你可以这样做,除了/可能例外),所以不做任何新的事情。并且并不真正期望它的参数 type ;它只是一个包装器。这些功能以及其他类似功能不提供任何额外的功能,而这些功能是 和 所不具备的。(例如,回到一个dynApplydynApptoDynfromDynacasttypeOfcastDynamic对您的问题不是很有用!)

3要查看实际的错误,您可以尝试编译以下完整的 Haskell 程序:

{-# LANGUAGE ExistentialQuantification #-}
import Data.Dynamic
import Data.Typeable
import Data.Maybe

randItem :: [a] -> IO a
randItem = return . head -- Good enough for a short and non-compiling example

dynListToList :: Typeable a => [Dynamic] -> [a]
dynListToList = mapMaybe fromDynamic

data TypeableList = forall a. Typeable a => TypeableList [a]

randList :: [Dynamic] -> IO TypeableList
randList dl = do
  tr <- randItem $ map dynTypeRep dl
  return . TypeableList $ dynListToList dl -- Error!  Ambiguous type variable.

果然,如果你尝试编译它,你会得到错误:

SO12273982.hs:17:27:
    Ambiguous type variable `a0' in the constraint:
      (Typeable a0) arising from a use of `dynListToList'
    Probable fix: add a type signature that fixes these type variable(s)
    In the second argument of `($)', namely `dynListToList dl'
    In a stmt of a 'do' block: return . TypeableList $ dynListToList dl
    In the expression:
      do { tr <- randItem $ map dynTypeRep dl;
           return . TypeableList $ dynListToList dl }

但是问题的重点是,您不能“添加修复这些类型变量的类型签名”,因为您不知道自己想要什么类型。

4大部分。GHC 7.4 支持将类型提升到种类和种类多态性;请参阅GHC 7.4 用户手册中的第 7.8 节“种类多态性和提升”。这不会使 Haskell 依赖类型化——类似TypeRep -> *example 的东西仍然没有5——但您将能够使用看起来像值Vec的非常富有表现力的类型来编写。

5从技术上讲,您现在可以写下看起来具有所需类型的内容:type family ToType :: TypeRep -> *. 但是,这需要提升kind类型,而不是type的;此外,您仍然无法实现它。(至少我不这么认为,我看不出你会怎么做——但我不是这方面的专家。)但在这一点上,我们还很遥远。 TypeRep TypeRep

于 2012-09-05T06:20:57.723 回答
13

您观察到的是该类型TypeRep实际上并没有携带任何类型级别的信息。只有术语级别的信息。这是一种耻辱,但是当我们知道我们关心的所有类型构造函数时,我们可以做得更好。例如,假设我们只关心Ints、列表和函数类型。

{-# LANGUAGE GADTs, TypeOperators #-}

import Control.Monad

data a :=: b where Refl :: a :=: a
data Dynamic where Dynamic :: TypeRep a -> a -> Dynamic
data TypeRep a where
    Int   :: TypeRep Int
    List  :: TypeRep a -> TypeRep [a]
    Arrow :: TypeRep a -> TypeRep b -> TypeRep (a -> b)

class Typeable a where typeOf :: TypeRep a
instance Typeable Int where typeOf = Int
instance Typeable a => Typeable [a] where typeOf = List typeOf
instance (Typeable a, Typeable b) => Typeable (a -> b) where
    typeOf = Arrow typeOf typeOf

congArrow :: from :=: from' -> to :=: to' -> (from -> to) :=: (from' -> to')
congArrow Refl Refl = Refl

congList :: a :=: b -> [a] :=: [b]
congList Refl = Refl

eq :: TypeRep a -> TypeRep b -> Maybe (a :=: b)
eq Int Int = Just Refl
eq (Arrow from to) (Arrow from' to') = liftM2 congArrow (eq from from') (eq to to')
eq (List t) (List t') = liftM congList (eq t t')
eq _ _ = Nothing

eqTypeable :: (Typeable a, Typeable b) => Maybe (a :=: b)
eqTypeable = eq typeOf typeOf

toDynamic :: Typeable a => a -> Dynamic
toDynamic a = Dynamic typeOf a

-- look ma, no unsafeCoerce!
fromDynamic_ :: TypeRep a -> Dynamic -> Maybe a
fromDynamic_ rep (Dynamic rep' a) = case eq rep rep' of
    Just Refl -> Just a
    Nothing   -> Nothing

fromDynamic :: Typeable a => Dynamic -> Maybe a
fromDynamic = fromDynamic_ typeOf

以上都是很标准的。有关设计策略的更多信息,您需要阅读 GADT 和单例类型。现在,您要编写的函数如下;这种类型看起来有点愚蠢,但请耐心等待。

-- extract only the elements of the list whose type match the head
firstOnly :: [Dynamic] -> Dynamic
firstOnly [] = Dynamic (List Int) []
firstOnly (Dynamic rep v:xs) = Dynamic (List rep) (v:go xs) where
    go [] = []
    go (Dynamic rep' v:xs) = case eq rep rep' of
        Just Refl -> v : go xs
        Nothing   ->     go xs

在这里,我们选择了一个随机元素(我掷了一个骰子,结果是 1),并且只从动态值列表中提取了具有匹配类型的元素。现在,我们可以Dynamic对标准库中的常规无聊旧版本做同样的事情;但是,我们无法以有意义的方式使用 the TypeRep。我现在证明我们可以这样做:我们将在 上进行模式匹配TypeRep,然后在TypeRep告诉我们的特定类型处使用封闭的值。

use :: Dynamic -> [Int]
use (Dynamic (List (Arrow Int Int)) fs) = zipWith ($) fs [1..]
use (Dynamic (List Int) vs) = vs
use (Dynamic Int v) = [v]
use (Dynamic (Arrow (List Int) (List (List Int))) f) = concat (f [0..5])
use _ = []

请注意,在这些等式的右侧,我们使用不同的具体类型的包装值;上的模式匹配TypeRep实际上是在引入类型级别的信息。

于 2012-09-05T07:13:14.507 回答
3

您需要一个根据运行时数据选择不同类型的值返回的函数。好,太棒了。但是类型的全部目的是告诉您可以对值执行哪些操作。当你不知道函数会返回什么类型时,你会如何处理它返回的值?您可以对它们执行哪些操作?有两种选择:

  • 您想读取类型,并根据它的类型执行一些行为。在这种情况下,您只能满足事先已知的有限类型列表,主要是通过测试“是这种类型吗?然后我们执行此操作......”。这在当前Dynamic框架中很容易实现:只需返回Dynamic对象,使用dynTypeRep过滤它们,然后将应用程序留给fromDynamic任何想要使用您的结果的人。Dynamic此外,如果您不介意在生产者代码而不是消费者代码中设置类型的有限列表,则很可能没有data Thing = Thing1 Int | Thing2 String | Thing3 (Thing,Thing). 如果可能的话,后一种选择是迄今为止最好的。
  • 您希望执行一些适用于一系列类型的操作,其中可能有一些您还不知道,例如通过使用类型类操作。这更棘手,在概念上也很棘手,因为您的程序不允许根据某些类型类实例是否存在来改变行为- 这是类型类系统的一个重要属性,即引入新实例可以使程序类型检查或停止类型检查,但它不能改变程序的行为。因此,如果您的输入列表包含不适当的类型,您就不能抛出错误,所以我真的不确定您可以做的任何事情本质上并不涉及在某个时候回退到第一个解决方案。
于 2012-09-05T12:51:10.000 回答