标签: gadt

我有一个很像这样的GADT:

data In a where
  M :: MVar a -> In a
  T :: TVar a -> In a
  F :: (a -> b) -> In a -> In b

它包装了各种输入原语,但最后一个构造函数也允许一个Functor实例:

instance Functor In where
  fmap f (F g v) = F (f . g) v
  fmap f x = F f x

这种类型的重点是BTW,它支持:

read :: In a -> IO a
read (M v) = takeMVar v
read (T v) = atomically (readTVar v)
read (F f v) = f …

请考虑以下代码:

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1

尽管有趣是一场详尽的比赛,但在使用-Wall进行编译时,GHC会抱怨丢失案例.但是,如果我添加另一个构造函数:

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A
  Baz …

Test.test中的错误似乎没有道理:

sealed trait A[-K, +V]
case class B[+V]() extends A[Option[Unit], V]

case class Test[U]() { 
  def test[V](t: A[Option[U], V]) = t match {
    case B() => null // constructor cannot be instantiated to expected type; found : B[V] required: A[Option[U],?V1] where type ?V1 <: V (this is a GADT skolem)
  }
  def test2[V](t: A[Option[U], V]) = Test2.test2(t)
}

object Test2 {
  def test2[U, V](t: A[Option[U], V]) = t match {
    case B() => null // This works
  }
}

有几种方法可以改变错误,或者消失: …

我正在玩ConstraintKindsGHC 的扩展.我有以下数据类型,它只是满足一个参数约束的一个框c:

data Some (c :: * -> Constraint) where
    Some :: forall a. c a => a -> Some c

例如,我可以构造一个带有某种数字的盒子(可能不是很有用).

x :: Some Num
x = Some (1 :: Int)

现在,只要c包含约束Show,我就可以提供一个实例Show (Some c).

instance ??? => Show (Some c) where
    show (Some x) = show x    -- Show dictionary for type of x should be in scope here

但是如何在实例上下文中标记此要求(标有???)？

我不能使用等式约束(c ~ Show),因为两者不一定相等.c可能是 …

Okasaki描述了可以使用该类型在Haskell中实现的持久实时队列

data Queue a = forall x . Queue
  { front :: [a]
  , rear :: [a]
  , schedule :: [x]
  }

增量旋转保持不变量

length schedule = length front - length rear

更多细节

如果您熟悉所涉及的队列,则可以跳过本节.

旋转功能看起来像

rotate :: [a] -> [a] -> [a] -> [a]
rotate [] (y : _) a = y : a
rotate (x : xs) (y : ys) a =
  x : rotate xs ys (y : a)

它由智能构造函数调用

exec :: [a] -> [a] -> [x] -> Queue …

在走向观察类型理论的"5.完整OTT"部分的最后,作者展示了如何在OTT中定义可构造的构造函数索引数据类型.这个想法基本上是将索引数据类型转换为参数化,如下所示:

data IFin : ? -> Set where
  zero : ? {n} -> IFin (suc n)
  suc  : ? {n} -> IFin n -> IFin (suc n)

data PFin (m : ?) : Set where
  zero : ? {n} -> suc n ? m -> PFin m
  suc  : ? {n} -> suc n ? m -> PFin n -> PFin m

康纳还在观察类型理论(交付)的底部提到了这种技术:

当然,解决方法是做GADT人员所做的事情,并明确地将归纳家族定义为命题平等.当然,你可以通过变性来运输它们.

但是,Haskell中的类型检查器知道范围中的等式约束,并且在类型检查期间实际使用它们.我们可以写

f :: a ~ b => a -> b
f x …

我开始在Haskell Wiki上阅读有关GADT的内容,但对它的理解并不是很清楚.您是否建议为Haskell初学者解释GADT的特定书籍章节或博客文章？

我发现我真的很喜欢将GADT与Data Kinds结合起来,因为它比以前更能提供类型安全性(对于大多数用途,几乎与Coq,Agda等人一样好).遗憾的是,模式匹配在最简单的示例中失败了,我认为除了类型类之外我无法编写我的函数.

这是一个解释我的悲伤的例子:

data Nat = Z | S Nat deriving Eq

data Le :: Nat -> Nat -> * where
    Le_base :: Le a a
    Le_S :: Le a b -> Le a (S b)

class ReformOp n m where
    reform :: Le (S n) (S m) -> Le n m

instance ReformOp a a where
    reform Le_base = Le_base

instance ReformOp a b => ReformOp a (S b) where
    reform (Le_S p) = Le_S $ reform p

class …

我希望一些Haskell专家可以帮助澄清一些事情.

是否有可能以Nat通常的方式定义(通过Haskell中的 @dorchard Singleton类型)

data S n = Succ n 
data Z   = Zero

class Nat n 
instance Nat Z
instance Nat n => Nat (S n)

(或其一些变体)然后定义一个LessThan关系,使得forall n和m

LessThan Z (S Z)
LessThan n m => LessThan n     (S m)
LessThan n m => LessThan (S n) (S m)

然后编写一个类似的函数:

foo :: exists n. (LessThan n m) => Nat m -> Nat n
foo (S n) = n
foo Z     = …

我有以下代码编译在我的程序中:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}

class (Show (Data a)) => HasData (a :: *) where
    type Data a :: *

data Foo :: * -> * where
    Foo :: (HasData a) => String -> Data a -> Int -> Foo a -- bunch of args

deriving instance Show (Foo a)

由于Foo构造函数的参数数量可以很多,我想使用记录语法编写代码,但我无法弄清楚如何使用GADT语法(GHC弃用的数据类型上下文,所以我试图避免它们) :

data Foo :: * -> * where
    Foo {
        getStr …