标签: gadt

我有这种类型和这些功能:

data Tag a where
    Tag :: (Show a, Eq a, Ord a, Storable a, Binary a) => a -> BL.ByteString -> Tag a

getVal :: Tag a -> a
getVal (Tag v _) = v

isBigger :: Tag a -> Tag a -> Bool
a `isBigger` b = (getVal a) > (getVal b)

代码没有做出类似的检查:

No instance for (Ord a)
  arising from a use of `>'
In the expression: (getVal a) > (getVal b)
In an equation for `isBigger':
    a …

我有这个代码片段,它使用了大量的GHC扩展:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Exts (Constraint)

data HList :: [*] -> * where
    Nil  :: HList '[]
    Cons :: a -> HList l -> HList (a ': l)

type family All (p :: * -> Constraint) (xs :: HList [*]) :: Constraint where
    All p Nil = ()
    All p (Cons x xs) = (p x, All p …

我一直在尝试使用rank-2类型在PureScript中编码GADT,如此处针对Haskell所述

我的代码看起来像:

data Z
data S n

data List a n 
  = Nil (Z -> n)
  | Cons forall m. a (List a m) (S m -> n)

fw :: forall f a. (Functor f) => (forall b . (a -> b) -> f b) -> f a
fw f = f id

bw :: forall f a. (Functor f) => f a -> (forall b . (a -> b) -> f b)
bw x f = map …

在ocaml手册第 7.20节的GADT基本示例中,'type a'的含义是什么？？为什么宣称"eval:一个术语 - > a"是不够的？

type _ term =
          | Int : int -> int term
          | Add : (int -> int -> int) term
          | App : ('b -> 'a) term * 'b term -> 'a term

        let rec eval : type a. a term -> a = function
          | Int n    -> n                 (* a = int *)
          | Add      -> (fun x y -> x+y)  (* a = int -> int -> int *)
          | …

我在编写解析器时遇到了问题.具体来说,我想成为不同类型的返回值.例如,我有两种不同的数据类型FA,PA代表两种不同的脂类 -

data FA = ClassLevelFA IntegerMass
        | FA           CarbonChain
        deriving (Show, Eq, Ord)

data PA   = ClassLevelPA       IntegerMass
          | CombinedRadylsPA   TwoCombinedRadyls
          | UnknownSnPA        Radyl Radyl
          | KnownSnPA          Radyl Radyl
          deriving (Show, Eq, Ord)

使用attoparsec,我已经构建了解析器来解析脂质速记符号.对于上面的数据类型,我有解析器faParser和paParser.我希望能够解析一个FA或PA.但是,由于FA和PA不同的数据类型,我不能做以下 -

inputParser =  faParser
           <|> paParser

我最近了解了GADT,我认为这可以解决我的问题.因此,我去做了一个GADT和一个eval函数并改变了解析器faParser和paParser.-

data ParsedLipid a where
  ParsedFA :: FA -> ParsedLipid FA
  ParsedPA :: PA -> ParsedLipid PA …

在长长的例子中提前道歉,我无法想出一个较短的例子.

让我们定义一个类型类Box,除了包含另一种类型之外什么都不做Content.

{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE TypeFamilies              #-}

class Box t where
    type Content t

data IntBox = IntBox
data StringBox = StringBox

我们来写一些例子:

instance Box IntBox where
    type Content IntBox = Int

instance Box StringBox where
    type Content StringBox = String

data JointBox a b = JointBox a b

instance (Box a, Box b) => Box (JointBox a b) where
    type Content (JointBox a b) = Either (Content a) (Content b)

到目前为止,这些都是编译和工作.输入GADT.我想要一个由一个盒子及其内容构成的代数数据类型.构造函数完全决定了框的类型.

data …

表达正常的数据类型(如列表和nat)非常简单,并且有很多例子.但是,翻译GADT的通用程序是什么？将典型类型(如Vector和依赖产品)从Idris转换为Morte的一些示例将非常具有说明性.

在下面的代码,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 T3 b where
  T3 :: { x3 :: a } -> T3 (F a)

我想知道为什么.T3只是T1有一个命名记录.这看起来并不那么特别,因为无论如何都可以使用构造函数语法来提取它.

这些示例可能看起来很愚蠢,但在我的代码中存在约束a,例如(Show a),因此可以在提取这些值时使用这些值.

我试图把我的头包裹在GADT周围,我怀疑一些魔法正在发生,我不明白.

考虑以下:

class C t

data T a where
  T :: (C a) => { getT :: a } -> T a

f :: C a => a -> ()
f = undefined

class D t where
  g :: t a -> ()

instance D T where
  g (T x) = f x

这一切都很好并且编译成功.

现在考虑T的稍微不同的实例定义:

instance D T where
  g x = f (getT x)

这看起来与上面完全相同,但是存在编译错误.这里发生了什么事？数据类型T没有存在变量,它只有一个简单的约束,它只是构造函数,但就是这样.

我一直在研究是否可以制作一个由操作和叶节点组成的非常简单的AST。但更具体地说，我希望能够将任何类型用作叶节点，而不是像这样在AST数据类型本身中明确指定它。

-- Instead of this
data Tree = Number Int | Word String | Operation Tree (Tree -> Tree -> Tree) Tree

-- I'd like something along the lines of this
data Tree a = Leaf a | Operation Tree (Tree -> Tree -> Tree) Tree

这不一定具有很大的实用性，但是我想看看是否有可能。到目前为止，我所管理的最接近的产品要求我对GADT的概念进行摸索：

{-# LANGUAGE GADTs #-}

data Tree l where
  Leaf :: l -> Tree l
  Operation :: Tree a -> (a -> b -> c) -> Tree b -> Tree c

let fivePlus2 = …