多态结果类型 GADT 函数答案

【问题标题】：Polymorphic result type GADT function多态结果类型 GADT 函数
【发布时间】：2017-01-22 09:36:19
【问题描述】：

在下面的代码中，我可以用什么替换x = ...。请注意，我不想对a 施加类限制（当然，a 已经是一种Bool，所以只能采用两种类型中的一种）。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data D (a :: Bool) where
  D1 :: D True
  D2 :: D False

x :: D a
x = ...

基本上，使用这样的 GADT，很容易对输入进行多态性（只需匹配适当的构造函数），但我想在输出中使用多态性。

【问题讨论】：

这是不可能的，没有办法返回D a中的多态值，除非它在底部。如果/当我们得到pi 类型（非擦除类型），那么就可以写x :: pi a. D a
此外，尽管令人不快，D Any 是一个有效类型。 DataKinds 仍然允许类型级别未定义...
我不介意未定义，只要定义了x :: D True 和x :: D False。
GHC 不知道a :: Bool 只能是True 或False。在a :: Bool 上调度是不可能的，因为它在运行时被删除。如果你想调度，你至少需要x :: SingI a => D a 或x :: Sing a -> D a。
@Clinton 显式字典被传递，类型被删除。例如，对于Show a => a -> IO () 之类的东西，它或多或少地实现为(a -> String) -> a -> IO ()。实际的类方法实现本身作为参数传入，因此类型不必如此。

标签： haskell types gadt

【解决方案1】：

这需要依赖类型 - 没有办法绕过它。在 Idris 中，一种类似 Haskell 的依赖类型语言，你可以这样写：

data D : Bool -> Type where
  D1 : D True
  D2 : D False

-- The `{ .. }` mean the argument is inferred.
x : {a : Bool} -> D a
x {a = True} = D1
x {a = False} = D2

在 Haskell 中，您可以在运行时基于类型进行调度的唯一方法是通过类型类，因此您需要一个约束。事实上，正如@András 指出的那样，SingI 就是为此而生的（它来自一个包 singletons，它正好处理了这类问题）。

在你的情况下，那将是：

{-# LANGUAGE GADTs, TypeInType, ScopedTypeVariables #-}

import Data.Singletons.Prelude   

data D (a :: Bool) where
  D1 :: D True
  D2 :: D False

x :: forall a. SingI a => D a
x = case sing :: Sing a of
      STrue -> D1
      SFalse -> D2

可能值得一提的是，尽管有 SingI 约束，但它已经定义了所有适当的实例。任何其他有效的D 类型但不带有Bool 参数的东西（如D Any）在编译时都会失败（根本找不到SingI 实例）。

ghci> let _ = x :: D True
ghci> let _ = x :: D False
ghci> let _ = x :: D Any
<interactive> error:
  • No instance for (SingI Any) arising from a use of ‘x’
  • In the expression: x :: D Any
    In a pattern binding: _ = x :: D Any

【讨论】：

这个答案将通过类型类技术的演示得到改进。
@BenjaminHodgson 已相应更新。