个人中心
文章发布
退出
作者热门文章
- html - 出于某种原因，IE8 对我的 Sass 文件中继承的 html5 CSS 不友好？
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景？
25
4
<分区>
我想使用 GADT 的规范示例创建一个异构表达式列表。
给定以下类型:
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 a = [Value (Bool true); Value (Int 1);]
这似乎是不可能的，因为它返回以下错误消息:
Error: This expression has type int value
but an expression was expected of type bool value
Type int is not compatible with type bool
有办法吗？
我查看了 ocaml documentation for GADT要么无法找到，要么无法理解如何找到。
有人能给我指出一些东西来解释为什么你不能用 GADT 做你能用 ADT 做的一切吗？
25
4
0
这三者之间有什么/为什么有区别？ GADT(和常规数据类型)只是数据系列的简写吗？具体有什么区别: data GADT a where MkGADT :: Int -> GADT Int dat
我们能否将构造函数没有给定约束的 GADT 转换为具有上述约束的 GADT？我想这样做是因为我想要深度嵌入箭头，并使用(目前)似乎需要 Typeable 的表示来做一些有趣的事情。 (One reas
我试图将 mod-n 计数器表示为将间隔 [0, ..., n-1] 分成两部分: data Counter : ℕ → Set where cut : (i j : ℕ) → Counter (
这是一个示例代码: {-# LANGUAGE GADTs #-} data NumGadt a where NumGadt :: Num a => a -> Int -> String -> Bo
我为表达式创建了一个 GADT。当我对具有约束的构造函数进行模式匹配时，类型检查器无法推断构造函数约束中使用的类型变量的约束。我认为代码和错误消息更清楚。 {-# LANGUAGE GADTs, Mu
背景 我正在使用 Haskell 编写一个红黑树实现 依赖类型并且我在理解为什么下面的代码不起作用时遇到了一些麻烦。作为一种热身练习，我想做的是找到一个给定任意值的子树。不幸的是，我在编译代码并最终继
在他的论文 Generics for the Masses Hinze 回顾了数据类型的编码。 从 Nat 开始 data Nat :: ⋆ where Zero :: Nat Succ
当我尝试创建一个返回 Thing a 的函数时，我目前正与类型检查器发生冲突。 (其中 Thing 是 GADT)。一个最小的人为例子: {-#LANGUAGE GADTs, EmptyDataDec
考虑以下代码 data Foo f where Foo :: Foo Int class DynFoo t where dynFoo :: Foo f -> Foo t instance Dy
假设我正在编写一个 DSL，并希望同时支持幻像类型和错误类型的表达式。我的值(value)类型可能是 {-# LANGUAGE GADTs, DataKinds #-} data Ty = Num |
当answering a question with a suggestion to use GADTs ，评论中出现了一些关于性能的问题。问题涉及类型类 PlotValue : class Plot
我只是在阅读Dependent Types at Work .在参数化类型的介绍中，作者提到在这个声明中 data List (A : Set) : Set where [] : List A
考虑以下代码: data (:+:) f g a = Inl (f a) | Inr (g a) data A data B data Foo l where Foo :: Foo A data
是分机GADT在 Haskell 中破坏多态性，即使在不使用 GADT 的代码中？ 这是一个有效但不使用 GADT 的示例 {-# LANGUAGE RankNTypes #-} --{-# LANG
这两个 GADT 声明之间有区别吗？ data A a b where ... data A :: * -> * -> * where ... 最佳答案 没有区别。有人可能会认为，在构
我在 haskell 中建立了一个几何库。我不打算发布它，它只是我用来提高我的语言知识的一个项目。 我有一个 Local数据类型，定义如下 data Local a where MkLocal
我正在阅读 GADTs for dummies Haskell Wiki 上的页面，我仍然不明白如何以及为什么应该使用它们。作者举了一个励志的例子: data T a where D1 ::
我正在解析表单的一些语句 v1 = expression1 v2 = expression2 ... 我正在使用 State Monad 并且我的状态应该是一对 (String, Expr a)，我真
如何使用广义代数数据类型？ haskell wikibook 中给出的示例太短了，无法让我深入了解 GADT 的真正可能性。 最佳答案 我发现“Prompt”monad(来自“MonadPrompt”
我正在使用 learnyouahaskell 来介绍 GADT，并且我对它们可能的用途很感兴趣。据我了解，它们的主要特点是允许显式类型设置。 如: data Users a where GetUs
我是一名优秀的程序员,十分优秀！