标签: gadt

任何人都可以给我提出有关在OCaml(3.12)中支持加法和减法操作的类型级整数的建议/建议吗？

例如,如果我有这样的数字:

type zero
type 'a succ
type pos1 = zero succ
type pos2 =  zero succ succ
...

我需要一种方法来定义类型的函数,如下所示:

val add: pos2 -> pos1 -> pos3

小背景:我正在尝试为物理维度上的操作移植一些haskell代码,并且我需要能够在维度类型上定义操作(记录7个类型级别的int代表7个基本SI单位的指数).我需要这样做以避免动态绑定(使用对象时)并使编译器能够静态地评估和检查所有这些表达式.

我目前的理解是我应该创建一个GADT来实现作为类型构造函数的操作,但我仍然在努力实现这个想法,任何提示都会受到高度赞赏.

有时候我需要返回存在量化类型的值.当我使用幻像类型时(例如表示平衡树的深度),这种情况最常发生.AFAIK GHC没有任何exists量词.它只允许存在量化的数据类型(直接或使用GADT).

举个例子,我想要这样的函数:

-- return something that can be shown
somethingPrintable :: Int -> (exists a . (Show a) => a)
-- return a type-safe vector of an unknown length
fromList :: [a] -> (exists n . Vec a n)

到目前为止,我有两个可能的解决方案,我将添加作为答案,我很高兴知道是否有人知道更好或不同的东西.

在我正在处理的HLearn库中,我有一些容器数据类型如下所示:

data (Model params model) => Container' params model = Container'
    { baseparams :: params
    , basemodel  :: model
    }

问题是,这种类型是尴尬,因为使用params并model都从独特的相互决定的:

class Model params model | params -> model, model -> params

因此,如果我在指定类型时不必指定它们,那将会更方便.编译器应该能够自动为我完成.

我解决这个问题的想法是创建一个使用存在量化的类型别名:

type Container model = forall params . (Model params model) => Container' params model

但这不起作用.如果我Container'像往常一样制作一个实例,一切正常:

data ContainerParams params = ContainerParams params

instance (Model params model) => Model (ContainerParams params) (Container' params model)

但是当我使用我的Container类型时:

instance (Model params …

假设我有以下代码:

{-# LANGUAGE GADTs, DeriveDataTypeable, StandaloneDeriving #-}
import Data.Typeable

class Eq t => OnlyEq t
class (Eq t, Typeable t) => BothEqAndTypeable t

data Wrapper a where
    Wrap :: BothEqAndTypeable a => a -> Wrapper a

deriving instance Eq (Wrapper a)
deriving instance Typeable1 Wrapper

然后,以下实例声明工作,没有约束t:

instance OnlyEq (Wrapper t)

并做我期望它做的事情.

但是以下实例声明不起作用:

instance BothEqAndTypeable (Wrapper t)

自GHC - 我使用7.6.1 - 抱怨说:

No instance for (Typeable t)
  arising from the superclasses of an instance declaration
Possible fix: …

你能否告诉我有没有为Enum类提供Haskell派生机制的扩展？我的意思是除了"nullary constructors"之外还有很多合理的情况.这个主题有什么作品吗？

这只是一个测试,所以我不太关心,但我有这些定义:

type z
type _ s
type (_, _, _) balance =
  | Less : (*?'a.*) ('a, 'a s, 'a s) balance
  | Same : (*?'b.*) ('b, 'b, 'b) balance
  | More : (*?'a.*) ('a s, 'a, 'a s) balance
type _ aVL =
  | Leaf : z aVL
  | Node : (*?'a, 'b, 'c.*)('a, 'b, 'c) balance * 'a aVL * int * 'b aVL ->
    ('c s) aVL

我收到"type _ aVL ="的错误:

Error: In this definition, a type …

我正在玩OCAMl中的GADT和幻像类型.我明白GADT是描述某些幻像类型的便利 - 如果我错了,请纠正我.所以我决定尝试将使用GADT类型的程序转换为具有ADT和幻像类型的程序.

我从这篇博客文章中选择了一个GADT程序作为起点.这是一个小的bool/int表达式求值器,这是它的要点:

module GADT = struct
  type _ value =
    | Bool : bool -> bool value
    | Int : int -> int value

  type _ expr =
    | Value : 'a value -> 'a expr
    | If : bool expr * 'a expr * 'a expr -> 'a expr
    | Eq : 'a expr * 'a expr -> bool expr
    | Lt : int expr * int expr -> bool expr

  let rec eval : …

我偶然发现了以下小问题.我正在使用Haskell记录语法和GADT:

{-# LANGUAGE GADTs #-}

data Test a where 
  Test :: {someString :: String, someData :: a} -> Test a

现在我想创建一个Test具有不同类型的新值someData,但是相同的值someString(为了证明记录更新语法的使用):

test :: Test a -> Test Bool
test t = t {someData = True}

假设我在Test构造函数中添加了另一个字段:

data Test a where 
  Test :: {someString :: String, someData :: a, someMoreData :: a} -> Test a

然后我必须更改两个字段以保持我的代码类型正确:

test :: Test a -> Test Bool
test t = t {someData = True, someMoreData = False} …

我有像这样的GADT:

data TType a where
    TInt  :: TType Int
    TBool :: TType Bool

我想要一个像这样的功能:

genTType :: Gen (TType a)

哪个可以生成TType类型的随机构造函数.我可以通过创建存在的合格数据类型来实现这一点

data AnyType = forall a . MkAnyType (TType a)

然后生成随机数0到1(包括)并AnyType根据整数值创建.像这样:

intToAnyType :: Int -> AnyType
intToAnyType 0 = MkAnyType TInt
intToAnyType 1 = MkAnyType TBool
intToAnyType _ = error "Impossible happened"

但这种方法对我来说有几个缺点:

1. 没有外部类型安全.如果我向TType数据类型添加另一个构造函数,我可能忘记修复测试,编译器不会警告我这一点.
2. 编译器无法阻止我写作intToAnyType 1 = MkAnyType TInt.
3. 我不喜欢这个error.Int类型太宽泛了我.让这种模式匹配详尽无遗是件好事.

我可以在Haskell中做些什么来消除尽可能多的缺点？最好使用此模块的发电机:

• https://hackage.haskell.org/package/hedgehog-0.5.1/docs/Hedgehog-Gen.html

这三者之间的差异是什么/为什么？GADT(和常规数据类型)只是数据系列的简写吗？具体来说有什么区别:

data GADT a  where
  MkGADT :: Int -> GADT Int

data family FGADT a
data instance FGADT a  where             -- note not FGADT Int
  MkFGADT :: Int -> FGADT Int

data family DF a
data instance DF Int  where              -- using GADT syntax, but not a GADT
  MkDF :: Int -> DF Int

(这些例子是否过于简化,所以我没有看到差异的微妙之处？)

数据系列是可扩展的,但GADT则不可扩展.OTOH数据族实例不得重叠.所以我无法声明另一个实例/任何其他构造函数FGADT; 就像我不能声明任何其他构造函数GADT.我可以声明其他实例DF.

通过这些构造函数上的模式匹配,等式的rhs确实"知道"有效载荷是Int.

对于类实例(我很惊讶地发现)我可以编写重叠实例来使用GADT:

instance C (GADT a) ...
instance {-# OVERLAPPING #-} C (GADT Int) ... …