Haskell中的程序化类型注释

Question

当元编程时,传递Haskell的类型系统信息可能是有用的(或必要的),这些信息是关于程序已知但在Hindley-Milner中不可推断的类型.是否有一个库(或语言扩展等)提供了执行此操作的工具 - 即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,编译器会告诉您它有一个"模糊类型"并要求您提供一个.但是你不能提供手动类型注释,因为在写入时不知道类型(并且可能会有所不同); 该类型在运行时是已知的,但是 - 虽然在类型系统中不能使用的形式(这里,所需的类型由值表示tr,TypeRep-see Data.Typeable表示详细信息).

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

基本上我正在寻找一个带有(伪)类型的函数,??? -> TypeRep -> a它接受Haskell类型系统未知类型的值,TypeRep然后说:"相信我,编译器,我知道我在做什么.这件事有价值以此为代表TypeRep." (注意,这不是什么unsafeCoerce.)

或者有什么完全不同的东西让我在同一个地方？例如,我可以设想一种允许分配类型变量的语言扩展,例如扩展的加强版本,支持范围类型变量.

(如果这是不可能或非常不切实际的,例如,它需要在可执行文件中包含一个完整的GHCi解释器 - 请尝试解释原因.)

Answer 1

不,你不能这样做.它的长短是因为你正在尝试编写一个依赖类型的函数,而Haskell不是一个依赖类型的语言; 你无法将你的TypeRep价值提升到一个真实的类型,所以没有办法记下你想要的功能的类型.为了更详细地解释这一点,我首先要说明为什么你说出这种类型的方式randList并没有多大意义.然后,我将解释为什么你不能做你想要的.最后,我将简要提及一些关于实际做什么的想法.

Existentials

您的类型签名randList并不意味着您想要它的意思.记住,Haskell中的所有类型变量都是普遍量化的

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

因此,我有权将其称为,比方说,randList dyns :: IO [Int]我想要的任何地方; 我必须能够为所有人 提供回报价值a,而不仅仅是为某些人提供 a.将此视为游戏,它是调用者可以选择的a,而不是函数本身.你想说什么(这不是有效的Haskell语法,虽然你可以通过使用存在数据类型¹将其转换为有效的Haskell )更像是

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

这承诺列表的元素是某种类型a,它是一个实例Typeable,但不一定是任何这样的类型.但即便如此,你也会遇到两个问题.首先,即使您可以构建这样的列表,您可以用它做什么？其次,事实证明你甚至无法在第一时间构建它.

既然您对存在主义列表元素的了解就是它们的实例Typeable,您可以用它们做什么？ 查看文档,我们看到只有两个函数²采用以下实例Typeable:

• typeOf :: Typeable a => a -> TypeRep,来自类型类本身(实际上,其中唯一的方法); 和
• cast :: (Typeable a, Typeable b) => a -> Maybe b(unsafeCoerce用其他方式实现,不能用其他方式编写).

因此,所有你知道在列表中元素的类型,你可以打电话typeOf和cast他们.既然我们永远无法用它们做任何其他事情,我们的存在主义也可能(同样,无效的Haskell)

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

如果我们应用typeOf并cast列出列表中的每个元素,存储结果,并丢弃现在无用的存在类型原始值,这就是我们得到的.显然,TypeRep这个列表的一部分没用.列表的后半部分也不是.由于我们回到了普遍量化的类型,调用者randList再次有权要求他们为他们选择的任何(有类型的)获得a Maybe Int,a Maybe Bool或a .(实际上,它们比以前有更多的功能,因为它们可以将列表的不同元素实例化为不同的类型.)但是他们无法弄清楚他们要转换的类型,除非他们已经知道它 - 你仍然丢失了您要保留的类型信息.Maybe bb

甚至撇开它们没用的事实,你根本无法在这里构建所需的存在类型.当您尝试返回存在类型列表(return $ dynListToList dl)时出现错误.您打算使用哪种特定类型dynListToList？回想一下dynListToList :: forall a. Typeable a => [Dynamic] -> [a]; 因此,randList负责采摘其 a dynListToList将要使用.但它不知道a要选哪个; 再次,这是问题的根源!因此,您尝试返回的类型未指定,因此模糊不清.³

依赖类型

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

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

但这还不够好; 的TypeRep和[a]没有在所有链接.而这正是你想要表达的:某种方式来链接TypeRep和a.

基本上,你的目标是写出类似的东西

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类型,其相应的类型对​​列表的元素进行分类.如果你能做到这一点,你就会被设定.但是toType :: TypeRep -> *在Haskell中完全不可能写入:这样做需要依赖类型的语言,因为它toType tr是一种依赖于值的类型.

这是什么意思？在Haskell中,值依赖于其他值是完全可以接受的; 这就是功能.值head "abc",例如,依赖于价值"abc".类似地,我们有类型构造函数,因此类型依赖于其他类型是可以接受的; 考虑Maybe Int,以及它如何依赖Int.我们甚至可以拥有依赖于类型的价值!考虑id :: a -> a.这实际上是一系列功能:id_Int :: Int -> Int,id_Bool :: Bool -> Bool等等.我们拥有哪一个取决于它的类型a.(所以,真的,id = \(a :: *) (x :: a) -> x虽然我们不能在Haskell中写这个,但我们可以使用语言.)

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

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

事实上,正如您所注意到的,您甚至无法记下所需的类型和用途unsafeCoerce.对于某些问题,你可以侥幸逃脱; 我们可以写下函数的类型,但只能通过作弊来实现它.这究竟是多么fromDynamic有效.但正如我们在上面看到的那样,在Haskell中甚至没有一个好的类型可以解决这个问题.虚toType函数允许你给程序一个类型,但你甚至不能记下toType类型!

现在怎么办？

所以,你不能这样做.你应该怎么做？我的猜测是你的整体架构并不适合Haskell,尽管我还没有看到它; Typeable并且Dynamic实际上并没有在Haskell程序中显示那么多.(正如他们所说的那样,或许你正在"用口音来讲Haskell".)如果你只有一组有限的数据类型需要处理,你可以将事物捆绑成一个普通的旧代数数据类型:

data MyType = MTInt Int | MTBool Bool | MTString String

然后你可以写isMTInt,只是使用filter isMTInt,或filter (isSameMTAs randomMT).

虽然我不知道它是什么,有可能是一个方式,你能 unsafeCoerce过这个问题的办法.但坦率地说,除非你真的,真的,真的,真的,真的,真的知道你在做什么,否则这不是一个好主意.即便如此,它可能不是.如果您需要unsafeCoerce,您会知道,这不仅仅是一件方便的事情.

我真的同意Daniel Wagner的评论:你可能想要从头开始重新思考你的方法.但是,由于我还没有看到你的架构,我不能说这意味着什么.也许还有另一个Stack Overflow问题,如果你可以提炼出具体的难度.

¹看起来如下:

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

但是,由于这些代码都没有编译,我认为写出来exists更清楚.

²从技术上讲,还有一些其他看起来相关的功能,例如toDyn :: Typeable a => a -> Dynamic和fromDyn :: Typeable a => Dynamic -> a -> a.然而,Dynamic或多或少是Typeables 的存在包装,依赖于typeOf和TypeRep知道何时unsafeCoerce(GHC使用一些特定于实现的类型unsafeCoerce,但你可以这样做,可能除了dynApply/ dynApp),所以toDyn不做任何新的事.并fromDyn没有真正期待它的类型论证a; 它只是一个包装cast.这些功能以及其他类似的功能不能提供任何额外的功能,而这些功能并不仅仅是typeOf和cast.(例如,回到 a Dynamic对你的问题不是很有用!)

³要查看操作中的错误,您可以尝试编译以下完整的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 }

但问题的全部内容,你不能 "添加修复这些类型变量的类型签名",因为你不知道你想要什么类型.

⁴主要是.GHC 7.4支持将类型提升为种类和种类多态性; 请参阅GHC 7.4用户手册中的第7.8节"种类多态性和促销".这并没有使Haskell依赖类型 - 像TypeRep -> *示例的东西仍然是⁵ - 但你可以Vec使用看起来像值的非常富有表现力的类型来编写.

⁵从技术上讲,你现在可以写下看起来像所需类型的东西:type family ToType :: TypeRep -> *.然而,这需要一个类型推广的一种 TypeRep,而不是一个值的的类型 TypeRep ; 此外,你仍然无法实现它.(至少我不这么认为,我看不出你会怎么做 - 但我不是这方面的专家.)但是在这一点上,我们还远远不够.

Answer 2

您所观察到的是该类型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标准库中的常规无聊来做同样的事情; 然而,我们无法做到的是以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实际上是引入类型级信息.