extensible-0.3.2: Extensible, efficient, lens-friendly data types

Copyright (c) Fumiaki Kinoshita 2015 BSD3 Fumiaki Kinoshita experimental non-portable None Haskell2010

Data.Extensible.Internal

Description

A bunch of combinators that contains magic

Synopsis

# Documentation

data Membership xs x Source

The position of `x` in the type level set `xs`.

Instances

 Typeable ([k] -> k -> *) (Membership k) Eq (Membership k xs x) Ord (Membership k xs x) Show (Membership k xs x)

runMembership :: Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r Source

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

compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y) Source

Compare two `Membership`s.

ord :: Int -> Q Exp Source

Generates a `Membership` that corresponds to the given ordinal (0-origin).

data NavHere xs x where Source

Ensure that the first element of `xs` is `x`

Constructors

 Here :: NavHere (x : xs) x

navigate :: (NavHere xs x -> r) -> (Membership (Half (Tail xs)) x -> r) -> (Membership (Half (Tail (Tail xs))) x -> r) -> Membership xs x -> r Source

PRIVILEGED: Navigate a tree.

here :: Membership (x : xs) x Source

The `Membership` points the first element

navNext :: Membership xs y -> Membership (x : xs) y Source

The next membership

navL :: Membership (Half xs) y -> Membership (x : xs) y Source

Describes the relation of `Membership` within a tree

navR :: Membership (Half (Tail xs)) y -> Membership (x : xs) y Source

Describes the relation of `Membership` within a tree

data h :* s where Source

The type of extensible products.

Constructors

 Nil :: h :* [] Tree :: !(h x) -> (h :* Half xs) -> (h :* Half (Tail xs)) -> h :* (x : xs)

Instances

 Typeable ((k -> *) -> [k] -> *) ((:*) k) WrapForall k * Eq h xs => Eq ((:*) k h xs) (Eq ((:*) k h xs), WrapForall k * Ord h xs) => Ord ((:*) k h xs) WrapForall k * Show h xs => Show ((:*) k h xs) WrapForall k * Monoid h xs => Monoid ((:*) k h xs) WrapForall k * Binary h xs => Binary ((:*) k h xs)

class Member xs x where Source

Methods

Instances

 ((~) * (Check k1 Nat x (Lookup k1 x xs)) (Expecting k one), ToInt k one) => Member k xs x

remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r Source

Remember that `Member xs x` from `Membership`.

type (∈) x xs = Member xs x Source

Unicode flipped alias for `Member`

data Nat Source

Type level binary number

Constructors

 Zero DNat Nat SDNat Nat

Instances

 ToInt Nat Zero ToInt Nat n => ToInt Nat (SDNat n) ToInt Nat n => ToInt Nat (DNat n)

class ToInt n where Source

Converts type naturals into `Word`.

Methods

theInt :: proxy n -> Word Source

Instances

 ToInt Nat Zero ToInt Nat n => ToInt Nat (SDNat n) ToInt Nat n => ToInt Nat (DNat n)

type family Lookup x xs :: [Nat] Source

Lookup types

Equations

 Lookup x (x : xs) = Zero : Lookup x xs Lookup x (y : ys) = MapSucc (Lookup x ys) Lookup x [] = []

type family ListIndex n xs :: k Source

Lookup types

Equations

 ListIndex Zero (x : xs) = x ListIndex (SDNat n) (y : xs) = ListIndex n (Half xs) ListIndex (DNat n) xs = ListIndex n (Half xs)

data Assoc k v Source

The kind of key-value pairs

Constructors

 k :> v

Instances

 Associate k k1 k2 v xs => Associated (Assoc k k) xs ((:>) k k k v)

type family AssocKeys xs :: [k] Source

Equations

 AssocKeys ((k :> v) : xs) = k : AssocKeys xs AssocKeys [] = []

class Associate k v xs | k xs -> v where Source

`Associate k v xs` is essentially identical to `(k :> v) ∈ xs` , but the type `v` is inferred from `k` and `xs`.

Methods

association :: Membership xs (k :> v) Source

Instances

 ((~) * (Check k Nat k2 (Lookup k k2 (AssocKeys k k1 xs))) (Expecting Nat one), ToInt Nat one, (~) (Assoc k k1) ((:>) k k1 k2 v) (ListIndex (Assoc k k1) one xs)) => Associate k k k v xs

class LookupTree n xs x | n xs -> x where Source

Methods

lookupTree :: Functor f => proxy n -> (h x -> f (h x)) -> (h :* xs) -> f (h :* xs) Source

Instances

 LookupTree k Zero ((:) k x xs) x LookupTree k (Pred n) (Half k (Tail k xs)) x => LookupTree k (DNat n) ((:) k t xs) x LookupTree k n (Half k xs) x => LookupTree k (SDNat n) ((:) k t xs) x

type family Succ x :: Nat Source

The successor of the number

Equations

 Succ Zero = SDNat Zero Succ (DNat n) = SDNat n Succ (SDNat n) = DNat (Succ n)

type family MapSucc xs :: [Nat] Source

Ideally, it will be 'Map Succ'

Equations

 MapSucc [] = [] MapSucc (x : xs) = Succ x : MapSucc xs

type family Pred n :: Nat Source

Equations

 Pred (SDNat Zero) = Zero Pred (SDNat n) = DNat n Pred (DNat n) = SDNat (Pred n) Pred Zero = Zero

type family Div2 n :: Nat Source

Equations

 Div2 (SDNat n) = n Div2 (DNat n) = n Div2 Zero = Zero

type family Half xs :: [k] Source

Interleaved list

Equations

 Half [] = [] Half (x : (y : zs)) = x : Half zs Half (x : []) = `[x]`

type family Head xs :: k Source

Equations

 Head (x : xs) = x

type family Tail xs :: [k] Source

Type-level tail

Equations

 Tail (x : xs) = xs Tail [] = []

lemmaHalfTail :: proxy xs -> p (x : Half (Tail xs)) -> p (Half (x : xs)) Source

GHC can't prove this

lemmaMerging :: p (Merge (Half xs) (Half (Tail xs))) -> p xs Source

GHC can't prove this

type family xs ++ ys :: [k] infixr 5 Source

Type level ++

Equations

 [] ++ ys = ys (x : xs) ++ ys = x : (xs ++ ys)

type family Map f xs :: [k] Source

Type level map

Equations

 Map f [] = [] Map f (x : xs) = f x : Map f xs

type family Merge xs ys :: [k] Source

Type level merging

Equations

 Merge (x : xs) (y : ys) = x : (y : Merge xs ys) Merge xs [] = xs Merge [] ys = ys

type family Concat xs :: [k] Source

Type level concat

Equations

 Concat [] = [] Concat (x : xs) = x ++ Concat xs

type family Check x xs Source

Elaborate the result of `Lookup`

Equations

 Check x `[n]` = Expecting n Check x [] = Missing x Check x xs = Ambiguous x

data Expecting a Source

A type sugar to make type error more readable.

data Missing a Source

A type sugar to make type error more readable.

data Ambiguous a Source

A type sugar to make type error more readable.

module Data.Proxy