多态结果类型GADT函数

Question

在以下代码中,我可以替换什么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,很容易在输入上做多态(只是在相应的构造函数上匹配),但我想在输出中使用多态.

Answer 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