对于模糊标题的道歉,这里有一些背景:http://themonadreader.files.wordpress.com/2013/08/issue221.pdf
上述问题中的GADT文章介绍了Nat类型和用于各种类型级列表函数的natSing类型(concat,!!,head,repeat等).对于其中的几个函数,有必要创建类型族来定义Nat类型的+和<.
data Nat = Zero | Succ Nat
data NatSing (n :: Nat) where
ZeroSing :: NatSing Zero
SuccSing :: NatSing n -> NatSing (Succ n)
data List (n :: Nat) a where
Nil :: List n a
Cons :: a -> List n a -> List (Succ n) a
无论如何,我已经编写了一个函数"list",它将普通[a]转换为a List n a,以方便调用者.这需要列表的长度作为输入,就像repeat(来自链接文章):
list :: [a] -> NatSing n -> List n a
list [] ZeroSing = Nil
list (x:xs) …我在用Glasgow Haskell Compiler, Version 7.8.3, stage 2 booted by GHC version 7.6.3.
我试图在Haskell中对List类型使用以下数据定义:
data Eq a => List a = Nil | Cons a (List a)
但是,-XDatatypeContexts默认情况下,该标志是必需的,已删除的,甚至是从语言中删除的.它被广泛视为语言的错误.我也不想为List的定义使用特殊标志,因为我试图复制现有列表类型的功能.然后我能够使用以下代码段:
data List a where
Nil :: List a
Cons :: Eq a => a -> List a -> List a
它运行正常.这个解决方案的明显问题是现在我需要使用-XGADTs标志,在这种情况下我仍然不想依赖它,因为内置版本的列表不需要运行.有没有办法限制其中的类型Cons,Eq a以便我可以比较两个列表,而无需编译器标志和不使用derived关键字？其余代码如下:
instance Eq (List a) where
(Cons a b) == (Cons c d) = (a == c) && (b == …我已经在Haskell编程了几个月了,我真的很享受它.我觉得我对monad,functor,pure等有了很好的把握.现在我已经使用了这个漂亮的类型系统了,因为它可以表达一些不正确的东西听起来对我来说太可怕了.Haskell允许您有时通过将数据属性移动到类型系统中来解决此问题.例如,使用GADT,您可以定义无法以不平衡方式构建的平衡树:
因此,您保证在树上实现的任何功能都将生成正确的树.但在其他情况下,我看不出如何限制类型级别的数据.
这是我正在考虑的具体情况.我想表示一个图表,其中每个边指向一个存在的节点.因此,如果仅存在节点1-4,则无法定义到节点5的边.对于DAG样式图我知道这样的事情但是对于带有周期的图没有看到这样的东西.我该如何表达这样的话？
我正在编写一个库来处理使用延迟评估的无限序列.为简洁起见,我使用广义代数数据类型(GADT)来断言Ord对序列中每个术语的索引的约束.因此,以下类型检查:
{-# LANGUAGE GADTs #-}
data Term ix cff where
Term :: (Ord ix) => ix -> cff -> Term ix cff
data Sequence ix cff where
Seq :: [Term ix cff] -> Sequence ix cff
f (Seq (Term i x:_)) (Seq (Term j y:_)) = i < j
{-
add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2)
where addAlong :: (ix …我认为GADT很棒,直到我尝试将任何"GADT表达式"的例子分散在互联网上使用.
传统的ADT以免费的Eq为幌子提供定义平等.在GADTs中获取此代码:
data Expr a where
(:+:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
(:-:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
(:*:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
(:/:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr a
(:=:) :: (Show a, Eq a) => Expr a -> Expr a -> Expr …我正在使用learnyouahaskell报道GADT,我对它们的可能用途很感兴趣.我知道它们的主要特征是允许显式类型设置.
如:
data Users a where
GetUserName :: Int -> Users String
GetUserId :: String -> Users Int
usersFunction :: Users a -> a
usersFunction (GetUserName id)
| id == 100 = "Bob"
| id == 200 = "Phil"
| otherwise = "No corresponding user"
usersFunction (GetUserId name)
| name == "Bob" = 100
| name == "Phil" = 200
| otherwise = 0
main = do
print $ usersFunction (GetUserName 100)
除了在使用这些数据类型时增加额外的类型安全性,GADT的其他用途是什么？
假设我有一个复杂的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 -> T
我想让这个数据类型显示而不必手动编写实例.问题是,因为Show不再是超类Num,所以添加一个简单deriving instance Show T对于编译器来说不足以推断它必须Show为所有内部隐藏类型参数添加约束.
对于每个隐藏类型参数,它输出类似的东西
Could not deduce (Show n) arising from a use of 'showsPrec'
from the context Num n
bound by a pattern with …to_c下面的函数由于在使用GADTs扩展编译时出现类型错误而被拒绝,我希望将其用于此处未显示的无关代码片段.
newtype Church = Church { unC :: forall a. (a -> a) -> a -> a }
to_c :: Int -> Church
to_c 0 = let f0 f c = c in Church f0
to_c n =
let fn f c = iterate f c !! n in Church fn
错误信息:
Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the …我正在编写一个编译器,我正在为我的IR使用GADT,但是我的其他所有东西都使用标准数据类型.我在从旧数据类型转换为GADT期间遇到了麻烦.我试图用下面的小/简化语言重新创建这种情况.
首先,我有以下数据类型:
data OldLVal = VarOL Int -- The nth variable. Can be used to construct a Temp later.
| LDeref OldLVal
data Exp = Var Int -- See above
| IntT Int32
| Deref Exp
data Statement = AssignStmt OldLVal Exp
| ...
我想将这些转换为这种中间形式:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
-- Note: this is a Phantom type
data Temp a = Temp Int
data Type = IntT
| PtrT Type
data Command where …我试图从运行时使用一些GADT参数,假设我已经使用DataKinds扩展来允许将数据提升为类型.即拥有
data Num = Zero | Succ Num
data Something (len :: Num) where
Some :: Something len
我想有功能
toNum :: Something len -> Num
对于任何人Some :: Something n将返回n:
toNum (s :: Something n) = n
哪个在Haskell中无效.有可能这样做吗？