多态性结果类型GADT函数

在下面的代码中，我可以替换什么x = ...。请注意，我不想对类别a设置类别限制（当然，a也是类型Bool，因此只能采用两种类型之一）。多态性结果类型GADT函数

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

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

x :: D a 
x = ...

基本上，像这样GADTs很容易做输入多态性（只匹配合适的构造函数），但我想在输出中使用多态。

来源

2017-01-22 Clinton

这是不可能的，没有办法返回'D a'中的多态值，除非它是底部。如果/当我们得到'pi'类型（非擦除类型），那么可以写'x :: pi a。 D a' – chi

此外，尽管令人不快，但“任何”都是有效的类型。 'DataKinds'仍然允许类型级未定义... – Alec

只要定义了'x :: D True'和'x :: D False'，我不介意未定义。 – Clinton

这需要依赖类型 - 它没有办法绕过它。在伊德里斯，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

来源

2017-01-22 10:58:02 Alec

这个答案将通过类型类技术的演示得到改进。 –

@BenjaminHodgson据此更新。 – Alec

多态性结果类型GADT函数

回答

相关问题