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

Copyright(c) Fumiaki Kinoshita 2015
LicenseBSD3
MaintainerFumiaki Kinoshita <fumiexcel@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

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) 
NFData (Membership k xs x) 

runMembership :: Membership (y : xs) x -> Either (x :~: y) (Membership xs x) 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

PRIVILEGED: Compare two Memberships.

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

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

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

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

class Member xs x where Source

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

Instances

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

type (∈) x xs = Member xs x Source

Unicode flipped alias for Member

data Nat Source

Constructors

Zero 
DNat Nat 
SDNat Nat 

Instances

class ToInt n where Source

Methods

theInt :: proxy n -> Word8 Source

Instances

type family Lookup x xs :: [Nat] Source

Equations

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

type family Succ x :: Nat Source

Equations

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

type family MapSucc xs :: [Nat] Source

Equations

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

type family Half xs :: [k] Source

Equations

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

type family Tail xs :: [k] Source

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

Equations

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

type family Map f xs :: [k] Source

Equations

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

type family Merge xs ys :: [k] Source

Equations

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

type family Concat xs :: [k] Source

Equations

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

type family Check x xs Source

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