我有一个关于Scala的类型构造函数的类型推理的问题.我正在运行Scala 2.9.1 ...
假设我定义了Tree:
sealed trait Tree[C[_], A]
case class Leaf[C[_], A](a: A) extends Tree[C, A]
case class Node[C[_], A](a: A, c: C[Tree[C, A]]) extends Tree[C, A]
并根据我的Tree定义定义了BinaryTree:
type Pair[A] = (A, A)
type BinaryTree[A] = Tree[Pair, A]
我现在可以定义一个BinaryTree整数:
val tree: BinaryTree[Int] = Node[Pair, Int](1, (Leaf(2), Leaf(3)))
这个问题是我必须在实例化时提供类型参数Node.
所以,如果这样做:
val tree: BinaryTree[Int] = Node(1, (Leaf(2), Leaf(3)))
我收到错误:
error: no type parameters for method apply: (a: A, c: C[Tree[C,A]])Node[C,A] in
object Node exist so that it can be applied …我正在阅读这里的 GADT介绍,我发现限制程序员创建只有正确类型的语法树很好的想法,我把这个想法放到我的简单lambda演算解释器中,但后来我意识到我无法解析字符串到这个语法树,因为一个解析函数需要返回不同类型的语法树,具体取决于输入.这是一个例子:
{-# LANGUAGE GADTs #-}
data Ident
data Lambda
data Application
data Expr a where
Ident :: String -> Expr Ident
Lambda :: Expr Ident -> Expr a -> Expr Lambda
Application :: Expr a -> Expr a -> Expr Application
在使用GADT之前,我使用的是:
data Expr = Lambda Expr Expr
| Ident String
| Application Expr Expr
GADT在这里很有优势,现在我无法创建无效的语法树Lambda (Application ..) ...
但是使用GADT,我无法解析字符串并创建解析树.以下是Lambda,Ident和Application表达式的解析器:
ident :: Parser (Expr Ident)
ident = ...
lambda :: Parser (Expr Lambda)
lambda = ... …我有以下代码,我希望这样的类型检查失败:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
import Control.Lens
data GADT e a where
One :: Greet e => String -> GADT e String
Two :: Increment e => Int -> GADT e Int
class Greet a where
_Greet :: Prism' a String
class Increment a where
_Increment :: Prism' a Int
instance Greet (Either String Int) where
_Greet = _Left
instance Increment (Either String Int) where
_Increment = _Right
run :: …请考虑以下代码
data Foo f where
Foo :: Foo Int
class DynFoo t where
dynFoo :: Foo f -> Foo t
instance DynFoo Int where
dynFoo Foo = Foo
obsFoo :: (DynFoo t) => Foo f -> Foo t
obsFoo = dynFoo
useDynFoo :: Foo f -> Int
useDynFoo (obsFoo -> Foo) = 1
模式匹配useDynFoo应限制使用obsFoo类型Foo f -> Foo Int,这应该使它搜索一个实例DynFoo Int.但是,它会搜索DynFoo t未知的实例t,并自然会失败.
No instance for (DynFoo t0) arising from a …这两个GADT声明之间有区别吗？
data A a b where
...
data A :: * -> * -> * where
...
考虑以下:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
data T = T1 | T2
data D (t :: T) where
D1 :: D T1
D2 :: D T2
D3 :: D d
D4 :: D T1
x1 :: [D T1]
x1 = [D1, D3, D4]
x2 :: [D T2]
x2 = [D2, D3]
基本上x1是所有有效构造函数的列表D T1,并且x2是所有有效构造函数的列表D T2.
但是,我希望这两个列表能够反映添加的任何其他构造函数D,我不想像现在这样对这些列表进行硬编码.
有没有办法定义x1并x2自动生成它们D？
我有非常无辜的代码
data Config = Config
{ cInts :: [Int]
, cStrings :: [String] }
instance Semigroup Config where
c1 <> c2 = Config
{ cInts = andCombiner cInts
, cStrings = andCombiner cStrings }
where
andCombiner field = field c1 <> field c2
它编译并正常工作.但是,如果我添加TypeFamilies或GADTs扩展我看到非常奇怪的错误:
.../Main.hs:19:22: error:
• Couldn't match type ‘Int’ with ‘[Char]’
Expected type: [String]
Actual type: [Int]
• In the ‘cStrings’ field of a record
In the expression:
Config {cInts = andCombiner cInts, cStrings …我正在尝试使用GADT来获得良好约束的类型,但是在编译期间无法处理某些依赖项 - 例如用户输入.让我们考虑遵循AVL树定义:
data Zero
data S a
data AVL depth where
Nil :: AVL Zero
LNode :: AVL n -> Int -> AVL (S n) -> AVL (S (S n))
RNode :: AVL (S n) -> Int -> AVL n -> AVL (S (S n))
MNode :: AVL n -> Int -> AVL n -> AVL (S n)
GADT的魔力确保每个AVL树都很平衡.我可以定义一些基本功能,如
singleton :: a -> AVL (S Zero) x
singleton a = MNode Nil a Nil
insert :: a -> AVL …在下面的代码中：
\nclass FD a b | a -> b\n\ndata Foo a where\n Foo :: FD a b => b -> Foo a\n\nunFoo :: FD a b => Foo a -> b\nunFoo (Foo x) = x\n根据常识，这应该可行，因为aGADT 和函数中的约束是相同的，并且它确定b，但是这不会编译并出现以下错误：
\xe2\x80\xa2 Couldn't match expected type \xe2\x80\x98b\xe2\x80\x99 with actual type \xe2\x80\x98b1\xe2\x80\x99\n \xe2\x80\x98b1\xe2\x80\x99 is a rigid type variable bound by\n a pattern with constructor:\n Foo :: forall a b. FD a b => b -> Foo a,\n in …