标签: gadt

我在omegagb的devlog上看到了这个片段:

data ExecutionAST result where
  Return :: result -> ExecutionAST result
  Bind :: (ExecutionAST oldres) -> (oldres -> ExecutionAST result) ->
          ExecutionAST result
  WriteRegister :: M_Register -> Word8 -> ExecutionAST ()
  ReadRegister :: M_Register -> ExecutionAST Word8
  WriteRegister2 :: M_Register2 -> Word16 -> ExecutionAST ()
  ReadRegister2 :: M_Register2 -> ExecutionAST Word16
  WriteMemory :: Word16 -> Word8 -> ExecutionAST ()
  ReadMemory :: Word16 -> ExecutionAST Word8

什么data ... where意思？我认为该关键字data用于定义新类型.

如何使用广义代数数据类型？

haskell wikibook中给出的示例太短,无法让我了解GADT的真正可能性.

今天,当在存在的GADT构造函数上进行匹配时,尝试使用延迟模式时出现编译器错误:

存在或GADT数据构造函数不能在惰性(〜)模式中使用

为什么会有这种限制？如果被允许,会发生什么"坏"的事情？

在Haskell中的类型安全可观察共享中 Andy Gill展示了如何在DSL中恢复Haskell级别上存在的共享.他的解决方案在data-reify包中实现.是否可以修改此方法以与GADT一起使用？例如,鉴于此GADT:

data Ast e where
  IntLit :: Int -> Ast Int
  Add :: Ast Int -> Ast Int -> Ast Int
  BoolLit :: Bool -> Ast Bool
  IfThenElse :: Ast Bool -> Ast e -> Ast e -> Ast e

我想通过将上面的AST转换为恢复共享

type Name = Unique

data Ast2 e where
  IntLit2 :: Int -> Ast2 Int
  Add2 :: Ast2 Int -> Ast2 Int -> Ast2 Int
  BoolLit2 :: Bool -> Ast2 Bool
  IfThenElse2 :: Ast2 Bool …

当我尝试使用proc语法(使用Netwire和Vinyl)对GADT 进行模式匹配时:

sceneRoot = proc inputs -> do
            let (Identity camera :& Identity children) = inputs 
            returnA -< (<*>) (map (rGet draw) children) . pure

我从ghc-7.6.3得到(相当奇怪的)编译器错误

  My brain just exploded
    I can't handle pattern bindings for existential or GADT data constructors.
    Instead, use a case-expression, or do-notation, to unpack the constructor.
    In the pattern: Identity cam :& Identity childs

当我将模式放在模式中时,我得到了类似的错误proc (...).为什么是这样？它不健全,还是只是未实现？

昨天的一个问题有一个定义HList(来自HList包)使用数据系列.基本上:

data family HList (l :: [*])
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)

pattern HCons x xs = HCons1 (x, xs)

而不是通常的(IMO更优雅和直观)GADT定义

data HList (l :: [*]) where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)

这是因为数据系列版本允许我们强制(我们只能强制执行HList (x ': xs)案例,因为它是a newtype instance,但这就足够了),而GADT只推断一个名义角色l(从而阻止任何强制).(我对上述问题的回答有一个具体的例子.)

HList在这个为期两年的问题中,讨论了GADT角色系统的失败问题.基本上,GHC会自动将任何"类GADT"类型变量标记为名义变量. …

我正在阅读一篇关于Haskell的研究论文以及如何实现HList,并想知道所描述的技术何时对于类型检查器是否可判定.另外,因为你可以用GADT做类似的事情,我想知道GADT类型检查是否总是可判定的.

如果你有它们我更喜欢引用,所以我可以阅读/理解解释.

谢谢!

我无法Eq为使用 GADT 实现的表达式实现以下类型安全 DSL的实例。

data Expr a where
  Num :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  Plus :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a -> Expr a
  Equal :: Eq a => Expr a -> Expr a -> Expr Bool

表达式可以是 typeBool或Int. 有文字的构造函数Bool，Num它们具有相应的类型。只能将Int表达式相加（构造函数Plus）。If表达式中的条件应具有类型，Bool而两个分支应具有相同的类型。还有一个相等表达式，Equal其操作数应该具有相同的类型，并且相等表达式的类型是Bool …

我只是在阅读工作中的依赖类型.在参数化类型的介绍中,作者在本声明中提到了这一点

data List (A : Set) : Set where
  []   : List A
  _::_ : A ? List A ? List A

Listis 的类型Set ? Set并且A成为两个构造函数的隐式参数,即.

[]   : {A : Set} ? List A
_::_ : {A : Set} ? A ? List A ? List A

好吧,我试着改写它有点不同

data List : Set ? Set where
  []   : {A : Set} ? List A
  _::_ : {A : Set} ? A ? List A …

在官方OCaml文档的"语言扩展"章节的GADT部分中,_ -> .引入了表格的驳斥案例.但是,我认为模式匹配已经是详尽无遗的,所以我不确定何时需要反驳案例.

文档中给出的示例如下:

type _ t =
  | Int : int t
  | Bool : bool t

let deep : (char t * int) option -> char = function
  | None -> 'c'
  | _ -> .

但即使是文件也表明这种驳斥案件是多余的.有没有一个例子,代码需要反驳案例进行类型检查？