码:
data Exp a = Const a | Eq (Exp a) (Exp a)
我希望Const a包含一个show类型的值,以便我可以在以后打印它.所以在C#中我会写:
class Const : Exp { IShow X; }
class Eq : Exp { Exp X, Y; }
我怎么能在Haskell做到这一点？
有人能指出我在Haskell中为GADT定义Typeable或Typeable1实例的一组很好的例子.
或者,有人可以向我展示如何为以下GADT定义Typeable(手动).
data V a where
Unit :: V ()
Pair :: V a -> V b -> V (a, b)
L :: V a -> V (Either a b)
R :: V b -> V (Either a b)
Fresh :: Int -> V a
或者,指向介绍该想法的论文的指针也会有所帮助.
首先,这是我的代码的最小示例:
{-# LANGUAGE GADTs #-}
-- package "url"
import Network.URL (exportURL, URL(..), URLType(..))
data MyURL a where
GalleryURL :: URL -> MyURL URL
PictureURL :: URL -> MyURL URL
url = URL { url_type = PathRelative,
url_path = "www.google.com",
url_params = []}
galleryURL = GalleryURL url
myExportURL :: MyURL a -> String
myExportURL (GalleryURL a) = exportURL a
myExportURL (PictureURL a) = exportURL a
main = print $ myExportURL galleryURL
我使用GADT来避免混合不同类型的URL.myExportURL所有类型的URL 的功能都相同.有没有办法使用这样的东西:
myExportURL (_ a) = exportURL a …我正在阅读有趣的幽灵类型.第一个练习询问为什么有必要为在幻影类型上运行的函数提供签名.虽然我无法提出一般原因,但我确实在以下示例中看到了一个问题:
data Expr a where
I :: Int -> Expr Int
B :: Bool -> Expr Bool
Add :: Expr Int -> Expr Int -> Expr Int
Eq :: (Eq a) => Expr a -> Expr a -> Expr Bool
whatIs (I _) = "an integer expression"
whatIs (Add _ _) = "an adition operation"
现在我明白whatIs上面有两种可能的类型,即:
Expr a -> String
和
Expr Int -> String
但是,编译器会给出错误:
• Couldn't match expected type ‘t’ with actual type ‘[Char]’ …这是我正在尝试编写代码的一个简化的,也许是愚蠢的例子(这更复杂,涉及列表长度的编译时编码).
鉴于以下内容:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
data D (a :: Bool) where
D :: Bool -> D a
我想要以下功能g:
g :: D a -> Bool
g (D x) = x == a
当然,这不会编译为a类型,而不是值.
这是一个可能的解决方案:
class C (a :: Bool) where
f :: D a -> Bool
instance C True where
f (D x) = x == True
instance C False where
f (D x) = x == False …{-# LANGUAGE GADTs #-}
module Main where
data CudaExpr x where
C :: x -> CudaExpr x
Add :: Num x => CudaExpr x -> CudaExpr x -> CudaExpr x
Sub :: Num x => CudaExpr x -> CudaExpr x -> CudaExpr x
Mul :: Num x => CudaExpr x -> CudaExpr x -> CudaExpr x
Div :: (Num x, Fractional x) => CudaExpr x -> CudaExpr x -> CudaExpr x
Eq :: (Eq x) => CudaExpr x -> CudaExpr …在以下代码中,我可以替换什么x = ....请注意,我不想对类进行限制a(当然,无论如何a都是类似的Bool,所以只能采用两种类型中的一种).
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data D (a :: Bool) where
D1 :: D True
D2 :: D False
x :: D a
x = ...
基本上,对于像这样的GADT,很容易在输入上做多态(只是在相应的构造函数上匹配),但我想在输出中使用多态.
我最近问过如何制作一个GADT实例的同源列表:函数返回 GADT 的任何构造函数的结果
TL;博士
{-#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
data SomeThing = forall a. SomeThing (Thing a)
combine :: [SomeThing]
combine = [Something $ Foo 1, SomeThing $ Bar "abc"]
现在,我在动态"展开"它们时遇到了一些麻烦.假设我们有这个(仍然是人为的,但更接近我的实际用例)代码:
{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where
-- Define a contrived GADT
data Thing a where
Thing :: TKind a -> …任何人都知道如何/可以Foo在此代码中扩展GADT :
{-# language GADTs #-}
{-# language DeriveGeneric #-}
{-# language DeriveAnyClass #-}
{-# language TemplateHaskell #-}
{-# language StandaloneDeriving #-}
import Prelude (Int, String, print, ($))
import Data.GADT.Show ()
import Data.GADT.Compare ()
import Data.Dependent.Map (DMap, fromList, (!))
import Data.Dependent.Sum ((==>))
import Data.GADT.Compare.TH (deriveGEq, deriveGCompare)
import Data.Functor.Identity (Identity)
data Foo a where
AnInt :: Foo Int
AString :: Foo String
deriveGEq ''Foo
deriveGCompare ''Foo
dmap1 :: DMap Foo Identity
dmap1 = fromList [AnInt ==> 1, …我最近在OCaml一直在与GADT挣扎.我正在尝试为一种简单的语言编写一个解释器,使用不同的术语:
type (_, _) term =
| Const : lit -> (state, value) term
| Var : ident -> (state, value) term
| Plus : expr * expr -> (state, value) term
| Equ : expr * expr -> (state, value) term
| Neg : expr -> (state, value) term
| Skip : (state, state) term
| Asn : ident * expr -> (state, state) term
| Seq : stat * stat -> (state, state) term
| If : expr …