多态性结果类型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很容易做输入多态性(只匹配合适的构造函数),但我想在输出中使用多态。
这需要依赖类型 - 它没有办法绕过它。在伊德里斯,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据此更新。 – Alec
这是不可能的,没有办法返回'D a'中的多态值,除非它是底部。如果/当我们得到'pi'类型(非擦除类型),那么可以写'x :: pi a。 D a' – chi
此外,尽管令人不快,但“任何”都是有效的类型。 'DataKinds'仍然允许类型级未定义... – Alec
只要定义了'x :: D True'和'x :: D False',我不介意未定义。 – Clinton