标签: gadt

在这段代码中有重复的片段:

insert x (AATree t) = case insert' x t of
    Same t -> AATree t
    Inc t  -> AATree t

insertBlack :: (Ord a) => a -> AANode Black (Succ n) a -> AnyColor (Succ n) a
insertBlack x (Black l y r)
    | x < y     = case insert' x l of
          Same l' -> AnyColor $ Black l' y r
          Inc  l' -> AnyColor $ skew l' y r
    | otherwise = case insert' x …

我创建了一个使用GADT和DataKinds的问题的一个非常简单的例子.我的实际应用显然更复杂,但这清楚地捕捉了我的情况的本质.我正在尝试创建一个可以返回Test类型的任何值(T1,T2)的函数.有没有办法实现这一目标,还是我进入了依赖类型的领域？这里的问题看起来很相似,但我无法从他们那里找到(或理解)我的问题的答案.我刚开始理解这些GHC扩展.谢谢.

类似的问题1

类似的问题2

{-# LANGUAGE GADTs, DataKinds, FlexibleInstances, KindSignatures #-}

module Test where

data TIdx = TI | TD

data Test :: TIdx -> * where
  T1 :: Int -> Test TI
  T2 :: Double -> Test TD

type T1 = Test TI
type T2 = Test TD

prob :: T1 -> T2 -> Test TIdx
prob x y = undefined

----这是错误---- Test.hs:14:26:

Kind mis-match

The first argument of `Test' should have kind `TIdx',

but `TIdx' has kind `*'

In …

我在Haskell中编写了以下线性代数向量

data Natural where
    Zero :: Natural
    Succ :: Natural -> Natural

data Vector n e where
    Nil :: Vector Zero e
    (:|) :: (Show e, Num e) => e -> Vector n e -> Vector (Succ n) e
infixr :|

instance Foldable -- ... Vector ..., but how do I implement this?

当我尝试实现时Foldable,我遇到了问题Zero并且Succ有不同的定义(即.*和* - >*).

这个问题有明显的解决方案吗？

我正在使用GADT为货币创建基本维度(如物理维度)系统.尺寸(例如美元,美元/欧元,欧元/美元)表示为幻像类型.我希望能够以例如"10.3USD"或"0EUR"的方式打印一定数量的货币,并使用Show打印例如"10.3USD/EUR"的费率.我不太确定如何解释我的问题,所以我将举例说明我是如何解决它的:

{-# LANGUAGE GADTs #-}

class (Show a) => Currency a where unphantom :: a

data USD = USD deriving Show
data EUR = EUR deriving Show

instance Currency USD where unphantom = USD
instance Currency EUR where unphantom = EUR

data Amount a where
  Amount :: Currency a => Float -> Amount a
instance Show (Amount a) where 
  show (Amount x) = show x ++ show (unphantom :: a)

data Rate a b where
  Rate :: (Currency a, Currency …

考虑下面的OCaml代码:

type mytype = My : 'a list * 'a -> mytype

let rec foo : int -> mytype =
    fun n -> if n < 0 then My([], 2)
        else let My(xs, y) = foo (n - 1)
        in My(3::xs, y)

OCaml解释器在最后一行给出了一个错误foo,说:

此表达式具有类型#1列表,但是期望类型为int list的表达式

类型#1与int类型不兼容

我可以通过添加类型参数来mytype使代码工作,这样就可以了

type _ mytype = My : 'a list * 'a -> 'a mytype
let rec foo : int -> 'a mytype =
...

但是,让我说我真的不想改变它的定义mytype.我可以写foo,假设我想保留该功能(由非工作代码直观地理解)行为？

此外,有人可以解释问题的根源,即为什么初始代码不进行类型检查？

如何在GADT上进行模式匹配？在这种情况下，我在使用Bigarray的GADT时遇到了麻烦。更具体地说，代码

let print_layout v = match Bigarray.Genarray.layout v with
    | Bigarray.C_layout -> Printf.printf "C layout\n"
    | Bigarray.Fortran_layout -> Printf.printf "Fortran layout\n"

无法编译错误消息

Error: This pattern matches values of type
         Bigarray.fortran_layout Bigarray.layout
       but a pattern was expected which matches values of type
         Bigarray.c_layout Bigarray.layout
       Type Bigarray.fortran_layout is not compatible with type
         Bigarray.c_layout 

它在抱怨这个Bigarray.Fortran_layout案子。如果我们看一下Bigarray我们看到，

type c_layout = C_layout_typ
type fortran_layout = Fortran_layout_typ
type 'a layout =
    C_layout : c_layout layout
  | Fortran_layout : fortran_layout layout

因此，这是GADT，我在模式匹配方面做错了。什么是工作版本print_layout？

在 Agda 中的依赖类型编程的第 4 页上，List定义如下

infixr 40 _::_
data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

我很难将头环绕在最后一行。前阵子学过一些 Haskell，所以对cons运算符比较熟悉。

那么，要么你有一个空列表，它是 type List A，或者你创建一个带有::type函数的新值A -> List A -> List A，它接受一些 type 元素A和一个 type 列表A并返回一个新列表？

这似乎是直觉，但这并没有映射到我所知道的递归数据类型定义的概念（来自haskell），例如

data Tree a = Leaf a | Branch (Tree a) (Tree a)

问题那么这是一种什么样的类型呢？这里涉及到Agda的哪些概念？

我正在阅读24 天 GHC 扩展的 Rank-N-Types 部分并遇到以下 GADT：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

import Data.Char

data Some :: * -> * where
    SomeInt  :: Int -> Some Int
    SomeChar :: Char -> Some Char
    Anything :: a -> Some a

unSome :: Some a -> a
unSome (SomeInt x) = x + 3
unSome (SomeChar c) = toLower c
unSome (Anything x) = x

unSome (someInt 2) -- 5

尽管unSome它的类型变量是多态的，但可以向编译器证明在这种SomeInt情况下，将三个添加到给定值是安全的。作者将这种类型称为细化。

现在我很好奇我是否可以用 Scrott …

我正在尝试建模"异构树",即.一棵树,其中节点有不同的"种类",每种"种类"都限制在它们可能包含的"种类"中:

type id = string
type block
type inline

type _ node =
  | Paragraph : id * inline node list -> block node
  | Strong : id * inline node list -> inline node
  | Text : id * string -> inline node

然后可以像这样定义树:

let document =
    Paragraph ("p1", [
      Text ("text1", "Hello ");
      Strong ("strong1", [
        Text ("text2", "Glorious")
      ]);
      Text ("text3", " World!")
  ])

通常这将使用针对节点的每个"种类"的单独变体来完成,但是我试图将其定义为GADT,以便能够使用在每种节点上模式匹配的高阶函数来操纵树:

function
  | Text ("text2", _) ->
    Some (Text ("text2", "Dreadful"))
  | _ …

我试图理解Heinrich Apfelmus 的文章操作Monad教程,他在那里使用GADTs很多.作为一项心理练习,我试图重写他的代码示例,以便他们不再使用GADT.我不能这样做,现在我知道这是因为我的技能有限,还是存在根本问题.

在r/haskell上, Edward Kmett说" 如果你有Rank N类型,你总是可以通过一个类将GADT转换为最终[sic]无标记表示. "

但是,如果我不想使用Rank N类型呢？我想,我必须牺牲一些东西,但我仍然能够做到.

所以,如果我愿意牺牲一些类型的安全性,使用幻像类型,类型类和诸如此类,那么我可以为表达式(有点)编写一个eval函数,如下所示,而不使用LANGUAGE扩展吗？

                           -- using GADTs :
data Expr = I Int  |       -- Int  -> Expr Int
            B Bool |       -- Bool -> Expr Bool
            Add Expr Expr  -- Expr Int -> Expr Int -> Expr Int
            Eq  Expr Expr  -- Expr 1   -> Expr a   -> Expr Bool