haskell - Haskell中的程序化类型注释

Question

当进行元编程时，将有关程序已知但在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的参数上没有类型注释的情况下，编译器将告诉您它具有“模糊类型”，并要求您提供一个。但是您不能提供手动类型注释，因为在写时类型未知(并且可能会有所不同)。但是，该类型在运行时是已知的-尽管是类型系统无法使用的形式(此处，所需的类型由值tr，TypeRep表示-有关详细信息，请参见Data.Typeable)。

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

基本上，我正在寻找具有(伪)类型??? -> TypeRep -> a的函数，该函数采用Haskell的类型系统未知的类型的值和TypeRep并说:“相信我，编译器，我知道我在做什么。此TypeRep表示的值。” (请注意，这不是unsafeCoerce所做的。)

还是有完全不同的东西让我拥有相同的位置？例如，我可以想象一种语言扩展，它允许分配类型变量，例如扩展版本的扩展版本，它启用了作用域类型变量。

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

Answer 1

不，你不能这样做。它的长处和短处是您正在尝试编写一个依赖类型的函数，而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的实例，因此您可以如何使用它们？ Looking at the documentation，我们看到只有两个函数2接受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的调用方再次有权要求他们为他们选择的任何(可键入的)Maybe Int获取Maybe Bool，Maybe b或b。 (实际上，它们具有比以前更大的功能，因为它们可以将列表的不同元素实例化为不同的类型。)但是，除非他们已经知道，否则他们无法弄清楚它们从哪个类型转换而来。丢失了您要保留的类型信息。

甚至不考虑它们没有用的事实，您根本无法在此处构造所需的存在类型。当您尝试返回存在类型的列表(return $ dynListToList dl)时出现错误。您以哪种特定类型调用dynListToList？回想一下dynListToList :: forall a. Typeable a => [Dynamic] -> [a];因此，randList负责选择要使用的a。但是它不知道选择哪一个dynListToList。再次，这就是问题的根源!因此，您尝试返回的类型是未指定的，因此模棱两可。3

依赖类型

好的，那么什么使这种存在性有用(并可能)呢？好吧，我们实际上有更多信息:不仅我们知道有一些a，我们还有其a。因此，也许我们可以将其打包:

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

但是，这还不够好。 TypeRep和TypeRep根本没有链接。这正是您要表达的内容:链接[a]和TypeRep的某种方法。

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

toType :: TypeRep -> *

在这里，a是所有类型的类型。如果您以前从未看过种类，那么它们就是要键入值。 *对类型进行分类，*对单参数类型构造函数进行分类，等等。(例如* -> *，Int :: *，Maybe :: * -> *和Either :: * -> * -> *。)

这样，您就可以编写代码(再次，该代码不是有效的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.

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

这是什么意思？在Haskell中，值依赖于其他值是完全可以接受的。这就是功能。例如，值toType tr取决于值head "abc"。同样，我们有类型构造函数，因此类型依赖于其他类型是可以接受的。考虑"abc"及其依赖于Maybe Int的方式。我们甚至可以拥有取决于类型的值!考虑Int。这实际上是一组函数:id :: a -> a，id_Int :: Int -> Int等。我们拥有的函数取决于id_Bool :: Bool -> Bool的类型。 (实际上是a；尽管我们无法在Haskell中编写此代码，但是有些语言可以。)

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

因此，在Haskell中，我们可以先检查有关类型的所有内容，丢弃所有信息，然后编译仅引用值的内容。实际上，这正是GHC所做的；由于我们永远无法在Haskell的运行时检查类型，因此GHC会在编译时删除所有类型，而不会更改程序的运行时行为。这就是为什么id易于实现(在操作上)并且完全不安全的原因:在运行时，它是空操作，但它属于类型系统。因此，在Haskell类型系统中完全不可能实现unsafeCoerce之类的东西。

实际上，正如您所注意到的，您甚至无法写下所需的类型并使用toType。对于某些问题，您可以避免这种情况。我们可以写下函数的类型，但只能通过作弊来实现。这就是unsafeCoerce的工作原理。但是正如我们在上面看到的，Haskell内部甚至没有一个很好的类型可以解决这个问题。虚构的fromDynamic函数允许您为程序指定类型，但您甚至无法写下toType的类型!

现在怎么办？

因此，您无法执行此操作。你该怎么办？我的猜测是，尽管我还没有看到，您的总体架构对于Haskell并不理想。实际上，在Haskell程序中toType和Typeable并没有显示太多。 (正如他们所说，也许您是“用Python的口音讲Haskell”。)如果您只需要处理一组有限的数据类型，则可以将其 bundle 到一个普通的旧代数数据类型中:

data MyType = MTInt Int | MTBool Bool | MTString String

然后，您可以编写Dynamic，而只需使用isMTInt或filter isMTInt即可。

尽管我不知道它是什么，但是您可能可以通过某种方式对这个问题进行filter (isSameMTAs randomMT)编码。但是坦率地说，除非您真的，真的，真的，真的，真的，真的知道自己在做什么，否则这不是一个好主意。即使这样，也可能不是。如果您需要unsafeCoerce，就会知道，这不只是一件方便的事情。

我真的同意Daniel Wagner's comment:您可能会想要从头开始重新考虑您的方法。再说一次，但是，由于我还没有看到您的体系结构，所以我不能说这意味着什么。如果您可以提取出具体的困难，那么也许还有另一个堆栈溢出问题。

1如下所示:

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

但是，由于这些代码都无法编译，因此我认为用unsafeCoerce编写起来更清晰。

2从技术上讲，还有一些其他看起来相关的功能，例如 exists 和 toDyn :: Typeable a => a -> Dynamic 。但是，fromDyn :: Typeable a => Dynamic -> a -> a或多或少是Dynamic周围的存在性包装器，依靠Typeable和typeOf s知道何时应使用TypeRep(GHC使用某些实现特定的类型和unsafeCoerce，但是您可以通过这种方式做到这一点，但unsafeCoerce可能是例外/ dynApply)，因此dynApp不会执行任何新操作。而且toDyn并不真正期望其类型为fromDyn的参数；它只是a的包装。这些功能以及其他类似功能无法提供cast和typeOf所无法提供的任何额外功能。 (例如，返回cast对您的问题不是很有用!)

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支持将类型提升到种类以及种类多态性。参见section 7.8, "Kind polymorphism and promotion", in the GHC 7.4 user manual。但这并不能使Haskell进行依赖类型的键入(例如Dynamic示例仍不存在)5，但是您将能够通过使用看起来像值的非常有表现力的类型来编写TypeRep -> *。

5从技术上讲，您现在可以写下看起来像所需类型的东西:Vec。但是，这采用了升级后的type family ToType :: TypeRep -> *类型的类型，而不是TypeRep类型的值；而且，您仍然无法实现它。 (至少我不这么认为，而且我不知道你会怎么做，但是我不是这方面的专家。)但是目前，我们还很遥远。