标签: gadt

我正在尝试将 GADT 与 DataKinds 结合使用，如下所示

{-# LANGUAGE KindSignatures, DataKinds, GADTs #-}\nmodule NewGadt where\n\ndata ExprType = Var | Nest\n\ndata Expr (a :: ExprType) where\n  ExprVar :: String -> Expr Var\n  ExprNest :: Expr a -> Expr Nest\n\ndata BaseExpr\n  = BaseExprVar String\n  | BaseExprNest BaseExpr\n\ntranslate :: BaseExpr -> Expr a\ntranslate (BaseExprVar id) = ExprVar id\ntranslate (BaseExprNest expr) = ExprNest $ translate expr\n

编译错误：

/home/elijah/code/monty/src/NewGadt.hs:15:32: error:\n    \xe2\x80\xa2 Couldn\'t match type \xe2\x80\x98a\xe2\x80\x99 with \xe2\x80\x98\'Var\xe2\x80\x99\n      \xe2\x80\x98a\xe2\x80\x99 is a rigid type variable bound …

编辑：我提出了一个更具体的问题。谢谢这里的回答者，我认为后续问题可以更好地解释我在这里引入的一些困惑。

TL;DR我正在努力将约束证明放入表达式中，同时在构造函数上使用具有存在约束的 GADT。（这是一个严肃的口，抱歉！）

我将问题归结为以下几点。我有一个简单的 GADT，它表示名为 的点X和名为 的函数应用程序F。点X被限制为Objects。

data GADT ix a where\n  X :: Object ix a => a -> GADT ix a\n  F :: (a -> b) -> GADT ix a -> GADT ix b\n

Constrained指的是其对象受某物约束的容器，并且Object是某物。（编辑：我真正的问题涉及Category约束类别Cartesian中的类）

-- | I can constrain the values within containers of …

语境

我想对 Web 应用程序的路由进行建模，使其满足以下要求：

1. 可以强制执行完整的定义
2. 可以创建不完整的定义
3. 可以检查不完整的定义是否“匹配”（即包含在）完整的定义。

作为使用的示例：

type root =
  | Fruit of fruit
  | Veggie of veggie
  
and fruit =
  | Apple of apple
  | Banana of banana
  
and veggie =
  | Carrot of carrot
  
and apple = { diameter: int; cultivar: string; }
and banana = { length: int }
and carrot = { length: int; color: [`Orange | `Purple] }

有了这个，我们可以轻松创建和执行完整的定义：

let complete = Fruit (Apple { diameter = 8; cultivar = "Golden Delicious" })

但无法创建不完整的定义 …

我为表达式创建了一个GADT.当我对具有约束的构造函数进行模式匹配时,类型检查器无法推断出对构造函数约束中使用的类型变量的约束.我认为代码和错误信息更具说明性.

{-# LANGUAGE GADTs, MultiParamTypeClasses #-}
import Data.Word

data Expr a where
  Value :: a -> Expr a
  Cast :: (Castable a b) => Expr a -> Expr b

class Castable a b where
  cast :: a -> b

instance Castable Word64 Word32 where
  cast = fromIntegral

instance (Show a) => Show (Expr a) where
  show (Cast e) = "Cast " ++ show e -- ERROR

我得到的错误:

gadt.hs:16:30:
    Could not deduce (Show a1) arising from a use of `show'
    from …

我想要一个简单的方法来创建一个String标记自己.现在我可以这样做:

data TagString :: Symbol -> * where
    Tag :: String -> TagString s
    deriving Show

tag :: KnownSymbol s => Proxy s -> TagString s
tag s = Tag (symbolVal s)

并使用它

tag (Proxy :: Proxy "blah")

但这并不好,因为

• 关于标签的保证仅tag由GADT提供.
• 每次我想创建一个值时,我都必须提供一个类型签名,如果值是某个更大表达式的一部分,它将变得难以处理.

有没有办法改善这一点,最好是朝着相反的方向,即从？String到Symbol？我想写,Tag "blah"并有ghc推断类型 TagString "blah".

GHC.TypeLits提供了someSymbolVal看起来有点相关的函数,但是它生成了SomeSymbola Symbol而不是a ,我可以完全掌握如何使用它.

我有两个文件：gadt1.ml和gadt2.ml，第二个取决于第一个。

gadt1.ml：

type never
type _ t1 = A1 : never  t1 | B1 : bool t1
type _ t2 = A2 : string t2 | B2 : bool t2
let get1 : bool t1 -> bool = function B1 -> true
let get2 : bool t2 -> bool = function B2 -> true

gadt2.ml：

let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> true
let get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true

当我使用ocaml …

数据Foo a定义如下:

data Foo a where
  Foo :: (Typeable a, Show a) => a -> Foo a
  -- perhaps more constructors

instance Show a => Show (Foo a) where
  show (Foo a) = show a

有些情况:

fiveFoo :: Foo Int
fiveFoo = Foo 5

falseFoo :: Foo Bool
falseFoo = Foo False

我如何定义任何函数b -> Foo a,例如:

getFoo :: (Show a, Typeable a) => String -> Foo a
getFoo "five" = fiveFoo
getFoo "false" = falseFoo

这里 …

我正在接受Simon Peyton-Jones关于GADT的讲座.在那里,声明了以下数据类型:

data T a where
  T0 :: Bool -> T Bool
  T1 :: T a

然后问的问题是以下函数的类型是什么:

f x y = case x of
          T0 _ -> True
          T1   -> y

对我来说,似乎唯一可能的类型是:

f :: T a -> Bool -> Bool

但是,以下类型:

f :: T a -> a -> a

也有效!确实你可以使用f如下:

 f (T1) "hello"

我的问题是为什么第二类签名f有效？

以下类型取自此问题

(* contains an error, later fixed by the OP *)
type _ task =
| Success : 'a -> 'a task
| Fail : 'a -> 'a task
| Binding : (('a task -> unit) -> unit) -> 'a task
| AndThen : ('a -> 'b task) * 'a task -> 'b task
| OnError : ('a -> 'b task) * 'a task -> 'b task

type _ stack =
| NoStack : 'a stack
| AndThenStack : …

假设我们想要构建一个表示典型操作的类型,比如说,一个无锁算法:

newtype IntPtr = IntPtr { ptr :: Int } deriving (Eq, Ord, Show)

data Op r where 
  OpRead :: IntPtr -> Op Int
  OpWrite :: IntPtr -> Int -> Op ()

  OpCAS :: IntPtr -> Int -> Int -> Op Bool

理想情况下,我们希望使用方便do注释在此模型中表示一些算法,例如(假设相应read = OpRead且cas = OpCAS出于美学原因)维基百科示例的以下几乎字面翻译:

import Prelude hiding (read)
import Control.Monad.Loops

add :: IntPtr -> Int -> Op Int
add p a = snd <$> do
  iterateUntil fst $ do …