代码之家 › 专栏 › 技术社区 › gspr

在haskell中生成haskell类型的设施(“二阶haskell”)?

type-safety typeclass metaprogramming types haskell

3

gspr · 技术社区 · 15 年前

如果这个问题有点含糊,请提前道歉。这是周末白日梦的结果。

有了Haskell出色的类型系统,将数学(尤其是代数)结构表示为类型类是令人愉快的。我是说,看看 numeric-prelude !但是,在实践中利用这种美妙的类型结构对我来说总是很困难的。

你有一个很好的,类型系统的表达方式 v1 和 v2 是向量空间的元素 V 还有那个 w 是向量空间的元素 W . 类型系统允许您编写程序添加 V1 和 V2 ,但不是 V1 和 W . 伟大的!但是在实践中,您可能希望使用可能有数百个向量空间,而且您当然不希望创建类型 V1 , V2 ,…, V100 a b c

fundeps

2 回复 | 直到 15 年前

1

8

John L 15 年前

Template Haskell wiki page Bulat's tutorials

mkFoo = [d| data Foo = Foo Int |]

data Foo = Foo Int $(mkFoo)

$(mkFoo 100) adaptive-tuple

Derive

2

5

luqui 15 年前

-- A family of types for the natural numbers
data Zero
data Succ n

-- A family of vectors parameterized over the naturals (using GADTs extension)
data Vector :: * -> * -> * where
    -- empty is a vector with length zero
    Empty :: Vector Zero a
    -- given a vector of length n and an a, produce a vector of length n+1
    Cons  :: a -> Vector n a -> Vector (Succ n) a

-- A type-level adder for natural numbers (using TypeFamilies extension)
type family Plus n m :: *
type instance Plus Zero n = n
type instance Plus (Succ m) n = Succ (Plus m n)

-- Typesafe concatenation of vectors:
concatV :: Vector n a -> Vector m a -> Vector (Plus n m) a
concatV Empty ys = ys
concatV (Cons x xs) ys = Cons x (concatV xs ys)

Agda Coq Epigram

concatV