标签: gadt

第一次尝试

很难让这个问题变得简洁,但是为了提供一个最小的例子,假设我有这种类型:

{-# LANGUAGE GADTs #-}
data Val where
  Val :: Eq a => a -> Val

这种类型让我愉快地构建以下异构外观列表:

l = [Val 5, Val True, Val "Hello!"]

但是,唉,当我写下一个Eq实例时,事情就出错了:

instance Eq Val where
  (Val x) == (Val y) = x == y -- type error

啊,我们Could not deduce (a1 ~ a).完全正确; 定义中没有任何内容表示x并且y必须是相同的类型.事实上,重点是允许它们不同的可能性.

第二次尝试

让我们Data.Typeable进入混合,只有尝试比较两者,如果他们碰巧是相同的类型:

data Val2 where
  Val2 :: (Eq a, Typeable a) => a -> Val2

instance Eq Val2 where
  (Val2 …

说我有以下GADT:

data Stage a b where
    Comb :: Stage a b -> Stage b c -> Stage a c
    FMap :: (a -> b) -> Stage a b

我现在想要一个像这样工作的函数:

run (a `Comb` b) = (a,b)
run (FMap f)     = (FMap f,FMap id)

我该如何构建这样的函数？

我尝试了不同的绑定类型的方法,但没有成功.是否存在我缺少的扩展,可以实现更广泛的类型绑定？

这是错误消息:

Couldn't match type `t' with `(Stage t1 b, Stage b t2)'
  `t' is a rigid type variable bound by
      the inferred type of run :: Stage t1 t2 -> t at <interactive>:11:5
In the expression: …

我有一个数据类型,其(单个)构造函数包含一个存在量化的类型变量:

data LogEvent = forall a . ToJSON a =>
            LogEvent { logTimestamp     :: Date
                     , logEventCategory :: Category
                     , logEventLevel    :: LogLevel
                     , logThreadId      :: ThreadId
                     , logPayload       :: a
                     }

当我最初编写该类型时,我隐藏了多态有效负载,因为我当时感兴趣的是输出到某个文件/流.但现在我想做更多有趣的事情,我需要观察它的实际类型a.

我从这个问题和其他读物中了解到,存在量化的类型变量在每个实例化时都是唯一的.但是,给定类型是ToJSON a我可以像下面这样(伪代码):

 let x :: Result Foo = fromJSON $ toJSON (logPayload event)

能够以更精确的类型转换为JSON和从JSON转换似乎很奇怪,尽管我可以理解其背后的基本原理.

那么logPayload如果我知道它的类型,如何重写该类型以允许提取？一世

我正在玩Haskell中的存在感和GADT,我正在尝试为组合器定义DSL(例如SKI).我有GADT工作,以及一个工作正常的减少功能(并且与问题无关)

{-# LANGUAGE GADTs, ExistentialQuantification #-}

import Control.Applicative
import Data.Monoid
import Control.Monad

data Comb t where
    S :: Comb ((a -> b -> c) -> (a -> b) -> a -> c)
    K :: Comb (a -> b -> a)
    I :: Comb (a -> a)
    B :: Comb ((b -> c) -> (a -> b) -> a -> c)
    C :: Comb ((b -> a -> c) -> a -> b -> c)
    W :: Comb ((a -> a …

我对 Haskell 的求和类型只有一个理论概念。然而我感觉到它们在 Haskell 中真的很重要，并且从根本上改变了你对数据建模的方式。因为我相信它们在动态类型语言中也很有用，所以我尝试在 Javascript 中实现一个合理的近似（我只对 Haskell 有肤浅的了解）。

这是一个或多或少有用的Namesum 类型示例，它能够处理各种名称格式。我知道 Haskell 区分类型构造函数和数据构造函数，并且可能有充分的理由进行这种区分。但是，我想不可能将这个概念映射到 Javascript。和模式匹配都不匹配。

无论如何，我的实际问题是：以下实现是否体现了和类型的性质以及它们在 Haskell 中的应用方式？

请注意：我不确定 SO 上是否欢迎此类跨语言问题。如果我应该避免它们，请告诉我。

// auxiliary functions

const A = f => x => f(x);
const show = api => api.show;

// the type constructor

const Name = (...xs) => A(({length: len}) => {
  switch (len) {
    case 1: {
      let [{length: len}] = xs; // no pattern matching but destructuring

      if (len > 1) { // no Char type in JS …

当我尝试创建一个返回函数Thing a（ThingGADT 在哪里）时，我目前正在与类型检查器进行斗争。一个最小的例子：

{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where

-- Define a contrived GADT
data TFoo
data TBar
data Thing a where
  Foo :: Int -> Thing TFoo
  Bar :: String -> Thing TBar

combine :: [Thing a]
combine = [Foo 1, Bar "abc"]

main :: IO ()
main = undefined

a类型检查器对不匹配感到不高兴TBar。想必这是因为它已经推断出来a了TFoo。但是，这是令人惊讶的，因为使用常规求和类型，您可以执行以下操作：

data Thing = Foo Int | Bar String

combine :: [Thing]
combine = [Foo 1, Bar …

存在性量化的数据构造像

data Foo = forall a. MkFoo a (a -> Bool)
         | Nil

可以很容易地翻译成GADT:

data Foo where 
    MkFoo :: a -> (a -> Bool) -> Foo
    Nil :: Foo

它们之间是否有任何差异:代码与一个而不是另一个编译,或者给出不同的结果？

我正在编写一个 Prolog 系统，并且使用多态变体来表示 Prolog 术语。

特别是，我使用多态变体（而不是常规变体），因此我可以进行子类型化，同时确保 OCaml 对子类型的匹配进行出色的详尽检查。

到目前为止，一切都很好！

我曾多次阅读过有关 GADT 的内容（在 Discuss.ocaml.org 和 realworldocaml.org 上）。对我来说，GADT 似乎提供了类似的功能，但内存占用更小：具有多个参数的情况的多态变体需要一个额外的指针，而常规变体不需要。

到目前为止，我还没有能够成功使用 GADT，所以这是我的问题：

是否有一种简单、直接的方法将使用多态变体的代码转换为 GADT？在一般情况下这甚至可能吗？

先感谢您！

Yoneda 只要设置了更高级别的扩展名，就具有有效的类型：

newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b)这产生了类型(forall b. (a -> b) -> f b) -> Yoneda f a。

b由消费者挑选Yoneda，因此不会出现在newtype声明的 LHS 上。

Coyoneda但是，对我来说没有意义：

data Coyoneda f a = forall b. Coyoneda (b -> a) (f b)这产生(b -> a) -> f b -> Coyoneda f a.

b被明确量化，但量词似乎不在正确位置呈现类型变量等级 2。 尽管如此b，并未在data声明的 LHS 中列出。那是什么？几乎是存在的？这只是一个没有受过教育的猜测，因为我不太了解存在量词，并假设 Haskell 不支持它们。

当我使用 GADT 语法定义新类型时，“普通”代数数据类型和广义代数数据类型之间到底有什么区别？我认为这与定义的数据构造函数的类型签名有关，但永远找不到确切的定义。

此外，这种差异的后果是什么，证明必须显式启用 GADT？我读到它们使类型推断变得不可判定，但是为什么我们不能将类型构造函数视为具有该类型签名的函数并将其插入推断算法呢？