Data.Extensible

This package defines an extensible type-indexed product type and a union type. Both are determined from the type-level list [k] and a wrapper k -> *. We can define ADTs not only for plain values, but also parameterized ones.

>>> let t = K0 (42 :: Int) <:* K0 "foo" <:* K0 (Just "bar") <:* Nil
>>> t
K0 42 <:* K0 "foo" <:* K0 (Just "bar") <:* Nil
>>> :t t
t :: K0 :* '[Int, [Char], Maybe [Char]]
>>> pluck t :: Int
42

Reexport

module Data.Extensible.Inclusion

module Data.Extensible.Match

module Data.Extensible.Plain

module Data.Extensible.Product

module Data.Extensible.Sum

Lookup

data Position xs x

The position of x in the type level set xs.

Instances

Typeable ([k] -> k -> *) (Position k)

Eq (Position k xs x)

Ord (Position k xs x)

Show (Position k xs x)

runPosition :: Position (y : xs) x -> Either (x :~: y) (Position xs x)

Embodies a type equivalence to ensure that the Position points the first element.

type (∈) x xs = Member xs x

Unicode flipped alias for Member

class Member xs x where

Member x xs or x ∈ xs indicates that x is an element of xs.

Methods

membership :: Position xs x

Instances

Record Nat (Lookup k x xs) => Member k xs x