标签: gadt

假设我们定义了一个GADT来比较类型:

data EQT a b where
  Witness :: EQT a a

然后可以使用以下类型签名声明函数eqt:

eqt :: (Typeable a, Typeable b) => a -> b -> Maybe (EQT a b)

... 如果typeOf x == typeOf y --- eqt xy评估为Just Witness,否则为Nothing？

函数eqt可以将普通的多态数据结构提升为GADT.

在回答有关使用GADT的建议的问题时,评论中提出了一些与性能有关的问题.问题涉及类型类PlotValue:

class PlotValue a where
    value :: a -> Double

我的回答建议使用GADT Input:

data Input where
    Input :: (PlotValue a, PlotValue b) => Maybe a -> Maybe b -> Input

但我认为细节并不重要.

我想知道性能的两个方面:

时间:模式匹配是否会产生任何运行时成本

case x of
    Input (Just a) (Just b) -> value a * value b
    _ -> 0.0

超过正常成本匹配两个Maybe值？

空间:类型值Input携带多少存储开销？我的猜测是它PlotValue为每个类型的值Input(每个都有一个'指针')带有两个字典,这意味着[Input]在内存使用方面,a比使用更低效,(Just Double, Just Double)或者更好的是,(# #Double, #Double #)- 如果你存储结果value …

假设我正在编写DSL并希望支持幻像类型支持和严重类型化表达式.我的价值类型可能是

{-# LANGUAGE GADTs, DataKinds #-}

data Ty = Num | Bool deriving (Typeable)

data Val a where
  VNum  :: Int  -> Val Num
  VBool :: Bool -> Val Bool

我可以使用幻影删除版本

{-# LANGUAGE ExistentialQuantification #-}

data Valunk = forall a . Valunk (V' a)

现在,我可以对值进行操作Valunk由case荷兰国际集团出既VNum和VBool,甚至以这种方式重新建立我的幻象类型

getNum :: Valunk -> Maybe (Val Num)
getNum (Valunk n@(VNum _)) = Just n
getNum _                   = Nothing

但这只是感觉我正在重新实现Typeable机器.不幸的是,GHC不会让我得出一个Typeable对Val

src/Types/Core.hs:97:13:
    Can't make …

假设我想用常数c,一元函数符号f和谓词P来表示一阶语言的有限模型.我可以将载体表示为列表m,将常量表示为元素m,将函数表示为有序列表元素对m(可以通过辅助函数应用ap),谓词作为m满足它的元素列表:

-- Models (m, c, f, p) with element type a
type Model a = ([a], a, [(a,a)], [a])

-- helper function application, assumes function is total
ap :: Eq a => [(a,b)] -> a -> b
ap ((x',y'):ps) x = if x == x' then y' else ap ps x

然后我可以在模型上构建特定的模型和操作.细节对于我的问题并不重要,只是类型(但我已经包含了定义,因此您可以看到类型约束的来源):

unitModel :: Model ()
unitModel = ([()], (), [((),())], [])

cyclicModel :: Int -> Model Int
cyclicModel n …

你如何使用GADT在OCaml中定义一个简单的lambda演算类DSL？具体来说,我无法弄清楚如何正确定义类型检查器以从无类型的AST转换为类型化的AST,也无法找出上下文和环境的正确类型.

下面是一些使用OCaml中传统方法的简单lambda演算语言的代码

(* Here's a traditional implementation of a lambda calculus like language *)

type typ =
| Boolean
| Integer
| Arrow of typ*typ

type exp =
| Add of exp*exp
| And of exp*exp
| App of exp*exp
| Lam of string*typ*exp
| Var of string
| Int of int
| Bol of bool

let e1=Add(Int 1,Add(Int 2,Int 3))
let e2=Add(Int 1,Add(Int 2,Bol false)) (* Type error *)
let e3=App(Lam("x",Integer,Add(Var "x",Var "x")),Int 4)

let rec typecheck con e …

我有一个ADT代表一个简单语言的AST:

data UTerm = UTrue
      | UFalse
      | UIf UTerm UTerm UTerm
      | UZero
      | USucc UTerm
      | UIsZero UTerm

这个数据结构可以表示不遵循语言类型规则的无效术语,例如UIsZero UFalse,我想使用强制类型良好的GADT:

{-# LANGUAGE GADTs #-}

data TTerm a where
  TTrue :: TTerm Bool
  TFalse :: TTerm Bool
  TIf :: TTerm Bool -> TTerm a -> TTerm a -> TTerm a
  TZero :: TTerm Int
  TSucc :: TTerm Int -> TTerm Int
  TIsZero :: TTerm Int -> TTerm Bool

我的问题是键入检查UTerm并将其转换为TTerm.我的第一个想法是UTerm -> Maybe (TTerm a),但这当然不起作用,因为它对所有人都无效a.我甚至不知道这种类型是什么,因为我们不知道 …

我经常有机会在Haskell中执行模运算,其中模数通常较大且通常为素数(如2000000011).目前,我只使用像(modAdd mab),(modMul mab),(modDiv mab)等函数.但这样做相当不方便,需要一个额外的参数来始终指定和携带并在常规积分中创建我的各种函数形式和单独的模型.

因此,创建一个类似这样的新类可能是个好主意:

class Integral a => Mod a

m = 2000000011

instance Integral a => Num (Mod a) where
   ... defining (+), etc. as modulo m

然后可以使用常规函数执行常规算术,并定义有用的结构,如

factorials :: [Mod Int]
factorials = 1:zipWith (*) factorials [1..]

但这有一个问题:Mod Int类型的所有值必须具有相同的模数.但是,我经常需要在一个程序中使用多个模数(当然总是只组合相同模数的值).

我想,但是不能完全理解,这可以通过以下方式克服:

class Integral a => Mod Nat a

其中Nat是一种以Peano方式编码模数的类型.这将是有利的:我可以具有不同模量的值,并且类型检查器将使我免于意外地组合该值.

这样的事情是否可行和有效？它是否会导致编译器或RTS尝试实际构建巨大的(Succ(Succ(重复...重复2000000011次)如果我尝试使用该模数,使解决方案无效？RTS是否会尝试检查在每个操作上都匹配类型吗？每个值的RTS表示是否会从一个只有一个未装箱的int中被炸毁？

有没有更好的办法？

结论

感谢来自cirdec,dfeuer,user5402和tikhon-jelvis的有用评论,我了解到(不出所料)我不是第一个有这个想法的人.特别是,Kiselyov和Shan 最近的一篇论文给出了一个实现,并且tikhon-jelvis向Hackage发布了一个名为(surprise!)模块算术的解决方案,它使用花哨的ghc pragma提供更好的语义.

开放式问题(对我而言)

幕后会发生什么？特别是,[Mod Int 2000000011]的百万元素清单是否会带来额外的200万份20000000左右？或者它是否编译为与一百万个Int的列表相同的代码,其中模数参数单独携带？后者会很好.

关于性能的补充

我对当前正在处理的问题进行了一些基准测试.第一次运行使用了未装箱的10,000元素Int向量,并对其执行了10,000次操作:

   4,810,589,520 bytes allocated …

F#是带有OOP的ML.它与Haskell广义代数数据类型和类型类最接近的是什么？

我有以下代码

{-# LANGUAGE DataKinds, GADTs, TypeOperators #-}

data Vect v a where
    Nil :: Vect '[] a
    Vec :: a -> Vect v a -> Vect (() ': v) a 

instance Eq a => Eq (Vect v a) where
    (==) Nil Nil               = True
    (Vec e0 v0) == (Vec e1 v1) = e0 == e1 && v0 == v1

在编译或解释时,-Wall给出以下警告:

Pattern match(es) are non-exhaustive
In an equation for `==':
    Patterns not matched:
        Nil (Vec _ _)
        (Vec _ …

这两个GADT声明之间有区别吗？

data A a b where
    ...

data A :: * -> * -> * where
    ...