Copyright | (c) Fumiaki Kinoshita 2015 |
---|---|
License | BSD3 |
Maintainer | Fumiaki Kinoshita <fumiexcel@gmail.com> |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
This package defines an extensible type-indexed product type and a union type.
Both are determined from the type-level list of elements which has kind [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
- data Position x xs
- runPosition :: Position x (y : xs) -> Either (x :~: y) (Position x xs)
- type (∈) = Member
- class Member x xs where
- data h :* s where
- (<:*) :: forall h x xs. h x -> (h :* xs) -> h :* (x : xs)
- unconsP :: forall h x xs. (h :* (x : xs)) -> (h x, h :* xs)
- hoistP :: (forall x. g x -> h x) -> (g :* xs) -> h :* xs
- outP :: forall h x xs. x ∈ xs => (h :* xs) -> h x
- sector :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> (h :* xs) -> f (h :* xs)
- sectorAt :: forall h x xs f. Functor f => Position x xs -> (h x -> f (h x)) -> (h :* xs) -> f (h :* xs)
- class Generate xs where
- data h :| s where
- (<:|) :: (h x -> r) -> ((h :| xs) -> r) -> (h :| (x : xs)) -> r
- exhaust :: (h :| []) -> r
- inS :: x ∈ xs => h x -> h :| xs
- picked :: forall f h x xs. (x ∈ xs, Applicative f) => (h x -> f (h x)) -> (h :| xs) -> f (h :| xs)
- class Include xs ys where
- newtype Match h a x = Match {
- runMatch :: h x -> a
- match :: (Match h a :* xs) -> (h :| xs) -> a
- mapMatch :: (a -> b) -> Match h a x -> Match h b x
- newtype K0 a = K0 {
- getK0 :: a
- (<%) :: x -> (K0 :* xs) -> K0 :* (x : xs)
- pluck :: x ∈ xs => (K0 :* xs) -> x
- bury :: x ∈ xs => x -> K0 :| xs
- (<%|) :: (x -> r) -> ((K0 :| xs) -> r) -> (K0 :| (x : xs)) -> r
- record :: forall f x xs. (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs) -> f (K0 :* xs)
- (<?%) :: (x -> a) -> (Match K0 a :* xs) -> Match K0 a :* (x : xs)
- newtype K1 a f = K1 {
- getK1 :: f a
- newtype Union fs a = Union {}
- liftU :: f ∈ fs => f a -> Union fs a
- (<?!) :: (f x -> a) -> (Match (K1 x) a :* xs) -> Match (K1 x) a :* (f : fs)
Lookup
Product
The extensible product type
(<:*) :: forall h x xs. h x -> (h :* xs) -> h :* (x : xs) infixr 5 Source
O(log n) Add an element to a product.
sector :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> (h :* xs) -> f (h :* xs) Source
O(log n) A lens for a specific element.
sectorAt :: forall h x xs f. Functor f => Position x xs -> (h x -> f (h x)) -> (h :* xs) -> f (h :* xs) Source
O(log n)
Sum
The extensible sum type
(<:|) :: (h x -> r) -> ((h :| xs) -> r) -> (h :| (x : xs)) -> r infixr 1 Source
O(1) Naive pattern match
picked :: forall f h x xs. (x ∈ xs, Applicative f) => (h x -> f (h x)) -> (h :| xs) -> f (h :| xs) Source
Inclusion/Permutation
Pattern match
Monomorphic
record :: forall f x xs. (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs) -> f (K0 :* xs) Source
O(log n) A lens for a plain value in a product.