在下面的代码中，我可以替换什么x = ...。请注意，我不想对类别a设置类别限制（当然，a也是类型Bool，因此只能采用两种类型之一）。 {-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data D (a :: Bool) where
D1 :: D True
在下面的代码编译错误，T1和T2编译罚款，但T3失败： {-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
type family F a
data T1 b where
T1 :: a -> T1 (F a)
data T2 b where
T2 :: { x2 :: a } -> T2 a
data T
自动获得节目实例假设我有一个复杂GADT与许多隐藏类型参数的构造函数： data T where
A :: Num n => n -> T
B :: (Num n, Integral m) => n -> m -> T
C :: Floating a => [a] -> T
-- and so on
Z :: Num n => n -> n ->
我试图建模一个“异构树”，即。一棵树，其中节点具有不同的“种”，每个“种”在孩子们的“种”被限制它们可能包含： type id = string
type block
type inline
type _ node =
| Paragraph : id * inline node list -> block node
| Strong : id * inline nod
几周前，我读了Writing an interpreter using fold。我尝试将这种方法应用到我正在处理的项目上，但由于GADT存在错误。这是产生相同问题的玩具代码。 {-# LANGUAGE GADTs, KindSignatures #-}
data Expr :: * -> * where
Val :: n -> Expr n
Plus :: Exp
此代码 {-# LANGUAGE GADTs #-}
data Expr a where
Val :: Num a => a -> Expr a
Eq :: Eq a => Expr a -> Expr a -> Expr Bool
eval :: Expr a -> a
eval (Val x) = x
eval (Eq x y) = (eval x) == (e
我想弄清楚类型类和GADTS之间的差异，特别是在使用-XMultiParamTypeClasses扩展名时。 似乎都具有类似用途： class MyClass a b where
f :: a -> b -> Bool
instance MyClass String String where
f s1 s2 = ...
instance MyClass Int Int
使用了一些扩展变量数，我可以做这样的事情： {-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
type family TF (a :: Bool) where
TF 'True = Int
TF