Safe Haskell	None
Language	Haskell2010

Kleene.Type

Contents

Regular expressions
- Tickless aliases
Heterogenous list
- Append and Split
Match
RE-indexed list
Inductions
- List structure
- RE structure
Conversion to Haskelly types.
Key
Lenses
Top

Description

Regular expression as types.

Synopsis

data RE a
- = E
- | V a
- | (RE a) :<> (RE a)
- | (RE a) :\/ (RE a)
- | S (RE a)
- | T
type E = E
type V = V
type S = S
type (<>) a b = a :<> b
type (\/) a b = a :\/ b
data HList :: [*] -> * where
- Nil :: HList '[]
- (:::) :: x -> HList xs -> HList (x ': xs)
hsingleton :: a -> HList '[a]
hlength :: HList xs -> Int
type family Append (xs :: [*]) (ys :: [*]) :: [*] where ...
append :: HList xs -> HList ys -> HList (Append xs ys)
split :: SList xs -> HList (Append xs ys) -> (HList xs, HList ys)
data SList :: [*] -> * where
- SNil :: SList '[]
- SCons :: forall x xs. SList xs -> SList (x ': xs)
class SListI (xs :: [*]) where
- slistI :: SList xs
hlistToSList :: HList xs -> SList xs
data Match :: RE * -> [*] -> * where
- MatchE :: Match E '[]
- MatchV :: forall a. Match (V a) '[a]
- MatchA :: forall re re' xs ys. SList xs -> Match re xs -> Match re' ys -> Match (re <> re') (Append xs ys)
- MatchL :: forall re re' xs. Match re xs -> Match (re \/ re') xs
- MatchR :: forall re re' xs. Match re' xs -> Match (re \/ re') xs
- MatchN :: forall re. Match (S re) '[]
- MatchC :: forall re xs ys. SList xs -> Match re xs -> Match (S re) ys -> Match (S re) (Append xs ys)
- MatchT :: forall xs. SList xs -> Match T xs
class MatchI (re :: RE *) (xs :: [*]) where
- justMatchIt :: Match re xs
matchE :: Match E '[]
matchV :: Match (V a) '[a]
matchA :: SListI xs => Match r xs -> Match s ys -> Match (r <> s) (Append xs ys)
matchL :: Match r xs -> Match (r \/ s) xs
matchR :: Match s xs -> Match (r \/ s) xs
matchN :: Match (S re) '[]
matchC :: SListI xs => Match r xs -> Match (S r) ys -> Match (S r) (Append xs ys)
withE :: x -> Match E xs -> HList xs -> x
withV :: (a -> x) -> Match (V a) xs -> HList xs -> x
withUnion :: (Match r xs -> HList xs -> x) -> (Match r' xs -> HList xs -> x) -> Match (r \/ r') xs -> HList xs -> x
withAppend :: (x -> y -> z) -> (forall xs. Match r xs -> HList xs -> x) -> (forall ys. Match r' ys -> HList ys -> y) -> Match (r <> r') zs -> HList zs -> z
withStarMon :: forall x r zs. Monoid x => (forall xs. Match r xs -> HList xs -> x) -> Match (S r) zs -> HList zs -> x
withStarR :: forall x y r zs. (x -> y -> y) -> y -> (forall xs. Match r xs -> HList xs -> x) -> Match (S r) zs -> HList zs -> y
withAppend3 :: (x -> y -> z -> w) -> (forall xs. Match r0 xs -> HList xs -> x) -> (forall ys. Match r1 ys -> HList ys -> y) -> (forall zs. Match r2 zs -> HList zs -> z) -> Match (r0 <> (r1 <> r2)) ws -> HList ws -> w
data REList :: RE * -> * where
- REList :: Match re xs -> HList xs -> REList re
mkREList :: MatchI re xs => HList xs -> REList re
withREList :: forall re x. REList re -> (forall xs. Match re xs -> HList xs -> x) -> x
withREListI :: forall re x. REList re -> (forall xs. MatchI re xs => HList xs -> x) -> x
class ListInduction (xs :: [*]) where
- listInduction :: f '[] -> (forall y ys. f ys -> f (y ': ys)) -> f xs
class ListInductionC (c :: * -> Constraint) (xs :: [*]) where
- listInductionC :: Proxy c -> f '[] -> (forall y ys. c y => f ys -> f (y ': ys)) -> f xs
listInductionP :: forall f xs. f '[] -> (forall y ys. f ys -> f (y ': ys)) -> SList xs -> f xs
class REInductionC (c :: * -> Constraint) (re :: RE *) where
- reInductionC :: Proxy c -> f '[] -> (forall x. c x => f '[x]) -> (forall xs ys. SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall xs. f xs -> f xs) -> (forall xs. f xs -> f xs) -> f '[] -> (forall xs ys. SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall xs. SList xs -> f xs) -> Match re zs -> f zs
reInductionP :: forall f re zs. f '[] -> (forall x. f '[x]) -> (forall xs ys. SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall xs. f xs -> f xs) -> (forall xs. f xs -> f xs) -> f '[] -> (forall xs ys. SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall xs. SList xs -> f xs) -> Match re zs -> f zs
haskelly :: Match re xs -> HList xs -> Haskelly re
type family Haskelly (re :: RE *) :: * where ...
data Key (s :: Symbol) = Key
key :: Key s -> Key s
keyVal :: KnownSymbol s => Key s -> String
rval :: Iso (REList (V a)) (REList (V b)) a b
rpair :: Iso (REList (a <> b)) (REList (c <> d)) (REList a, REList b) (REList c, REList d)
rfst :: Lens (REList (a <> c)) (REList (b <> c)) (REList a) (REList b)
rsnd :: Lens (REList (c <> a)) (REList (c <> b)) (REList a) (REList b)
rsum :: Iso (REList (a \/ b)) (REList (c \/ d)) (Either (REList a) (REList b)) (Either (REList c) (REList d))
rleft :: Prism (REList (a \/ c)) (REList (b \/ c)) (REList a) (REList b)
rright :: Prism (REList (c \/ a)) (REList (c \/ b)) (REList a) (REList b)
rstar :: Traversal (REList (S a)) (REList (S b)) (REList a) (REList b)
rnil :: Prism' (REList (S a)) ()
rcons :: Prism (REList (S a)) (REList (S b)) (REList a, REList (S a)) (REList b, REList (S b))
type T = T
matchT :: SListI xs => Match T xs
withTop :: y -> Match T zs -> HList zs -> y

Regular expressions

data RE a Source #

Regular expressions.

Constructors

E	empty string
V a	variable
(RE a) :<> (RE a) infixr 5	append
(RE a) :\/ (RE a) infixr 4	alternative
S (RE a)	star
T	top

Tickless aliases

type E = E Source #

type V = V Source #

type S = S Source #

type (<>) a b = a :<> b infixr 5 Source #

type (\/) a b = a :\/ b infixr 4 Source #

Heterogenous list

data HList :: [*] -> * where Source #

Heterogenous list

Constructors

Nil :: HList '[]
(:::) :: x -> HList xs -> HList (x ': xs) infixr 5

Instances

ListInductionC Show xs => Show (HList xs) Source #
Instance details Defined in Kleene.Type Methods showsPrec :: Int -> HList xs -> ShowS # show :: HList xs -> String # showList :: [HList xs] -> ShowS #

hsingleton :: a -> HList '[a] Source #

Create singleton HList.

hlength :: HList xs -> Int Source #

Append and Split

type family Append (xs :: [*]) (ys :: [*]) :: [*] where ... Source #

Equations

Append '[] ys = ys
Append (x ': xs) ys = x ': Append xs ys

append :: HList xs -> HList ys -> HList (Append xs ys) Source #

++ for HLists.

split :: SList xs -> HList (Append xs ys) -> (HList xs, HList ys) Source #

splitAt for HLists. We don't need Int, instead we need SList xs.

data SList :: [*] -> * where Source #

Type list's shape singleton. Needed for split.

Constructors

SNil :: SList '[]
SCons :: forall x xs. SList xs -> SList (x ': xs)

Instances

ListInduction xs => Show (SList xs) Source #
Instance details Defined in Kleene.Type Methods showsPrec :: Int -> SList xs -> ShowS # show :: SList xs -> String # showList :: [SList xs] -> ShowS #

class SListI (xs :: [*]) where Source #

Make compiler create SLists.

Methods

slistI :: SList xs Source #

Instances

SListI ([] :: [Type]) Source #
Instance details Defined in Kleene.Type Methods slistI :: SList [] Source #
SListI xs => SListI (x ': xs) Source #
Instance details Defined in Kleene.Type Methods slistI :: SList (x ': xs) Source #

hlistToSList :: HList xs -> SList xs Source #

Convert HList to SList.

Match

data Match :: RE * -> [*] -> * where Source #

Proof of match.

forall's are required, to better document the argument order for Core-term construction in the plugin.

Constructors

MatchE :: Match E '[]
MatchV :: forall a. Match (V a) '[a]
MatchA :: forall re re' xs ys. SList xs -> Match re xs -> Match re' ys -> Match (re <> re') (Append xs ys)
MatchL :: forall re re' xs. Match re xs -> Match (re \/ re') xs
MatchR :: forall re re' xs. Match re' xs -> Match (re \/ re') xs
MatchN :: forall re. Match (S re) '[]
MatchC :: forall re xs ys. SList xs -> Match re xs -> Match (S re) ys -> Match (S re) (Append xs ys) infixr 5
MatchT :: forall xs. SList xs -> Match T xs

Instances

Show (Match re xs) Source #
Instance details Defined in Kleene.Type Methods showsPrec :: Int -> Match re xs -> ShowS # show :: Match re xs -> String # showList :: [Match re xs] -> ShowS #

Implicit match

class MatchI (re :: RE *) (xs :: [*]) where Source #

This class has no defined instances.

KleenePlugin can solve the constraints for you.

Methods

justMatchIt :: Match re xs Source #

Smart constructors

matchE :: Match E '[] Source #

matchV :: Match (V a) '[a] Source #

matchA :: SListI xs => Match r xs -> Match s ys -> Match (r <> s) (Append xs ys) Source #

matchL :: Match r xs -> Match (r \/ s) xs Source #

matchR :: Match s xs -> Match (r \/ s) xs Source #

matchN :: Match (S re) '[] Source #

matchC :: SListI xs => Match r xs -> Match (S r) ys -> Match (S r) (Append xs ys) infixr 5 Source #

Smart destructors

withE :: x -> Match E xs -> HList xs -> x Source #

We usually don't bother eliminate '()'.

withV :: (a -> x) -> Match (V a) xs -> HList xs -> x Source #

Like runIdentity for RE a

withUnion :: (Match r xs -> HList xs -> x) -> (Match r' xs -> HList xs -> x) -> Match (r \/ r') xs -> HList xs -> x Source #

Like either for r :\/ s.

withAppend Source #

Arguments

:: (x -> y -> z)
-> (forall xs. Match r xs -> HList xs -> x)	fst
-> (forall ys. Match r' ys -> HList ys -> y)	snd
-> Match (r <> r') zs
-> HList zs
-> z

Like uncurry for r :<> s.

withStarMon Source #

Arguments

:: Monoid x
=> (forall xs. Match r xs -> HList xs -> x)	to `Monoid`.
-> Match (S r) zs
-> HList zs
-> x

Like foldMap for RE r.

withStarR Source #

Arguments

:: (x -> y -> y)	cons
-> y	nil
-> (forall xs. Match r xs -> HList xs -> x)
-> Match (S r) zs
-> HList zs
-> y

Like foldr f z for RE r.

withAppend3 Source #

Arguments

:: (x -> y -> z -> w)
-> (forall xs. Match r0 xs -> HList xs -> x)	fst
-> (forall ys. Match r1 ys -> HList ys -> y)	snd
-> (forall zs. Match r2 zs -> HList zs -> z)	snd
-> Match (r0 <> (r1 <> r2)) ws
-> HList ws
-> w

RE-indexed list

data REList :: RE * -> * where Source #

RE-indexed list.

Constructors

REList :: Match re xs -> HList xs -> REList re

Instances

REInductionC Show re => Show (REList re) Source #
Instance details Defined in Kleene.Type Methods showsPrec :: Int -> REList re -> ShowS # show :: REList re -> String # showList :: [REList re] -> ShowS #
AsEmpty (REList (S a)) Source #
Instance details Defined in Kleene.Type Methods _Empty :: Prism' (REList (S a)) ()
Cons (REList (S a)) (REList (S b)) (REList a) (REList b) Source #
Instance details Defined in Kleene.Type Methods _Cons :: Prism (REList (S a)) (REList (S b)) (REList a, REList (S a)) (REList b, REList (S b))

mkREList :: MatchI re xs => HList xs -> REList re Source #

Smart-constructor using MatchI constraint.

Note: The REList uses Match, not MatchI as working with expicit Match is more expressive. At least until KleenePlugin can solve all possible MatchI constraints.

withREList :: forall re x. REList re -> (forall xs. Match re xs -> HList xs -> x) -> x Source #

>>> withREListI (REList matchV $ hsingleton True) $ withV not justMatchIt
False

withREListI :: forall re x. REList re -> (forall xs. MatchI re xs => HList xs -> x) -> x Source #

>>> withREListI (REList matchV $ hsingleton True) $ withV not justMatchIt
False

Inductions

There are two ways to write induction,

Using a structure proof, like SList. If we fold over HList, we could use it as a structure proof too; but for constucting it, we'd need SList. This is 'listInductionP.
The benefit of this approach is its simplicity. However, the drawback is that we need to define an auxiliary type family to provide constrained version. See All in generics-sop package (version 0.3).
Alternatively, we can define a type class directly parametrised by the type-level structure.
This way additional constraints for different constructors can be added naturally. See ListInducton and ListInductionC.

List structure

class ListInduction (xs :: [*]) where Source #

(Type-level) list induction.

Methods

listInduction Source #

Arguments

:: f '[]	case: `SNil`
-> (forall y ys. f ys -> f (y ': ys))	case: `SCons`
-> f xs

Instances

ListInduction ([] :: [Type]) Source #
Instance details Defined in Kleene.Type Methods listInduction :: f [] -> (forall y (ys :: [Type]). f ys -> f (y ': ys)) -> f [] Source #
ListInduction xs => ListInduction (x ': xs) Source #
Instance details Defined in Kleene.Type Methods listInduction :: f [] -> (forall y (ys :: [Type]). f ys -> f (y ': ys)) -> f (x ': xs) Source #

class ListInductionC (c :: * -> Constraint) (xs :: [*]) where Source #

Constrained ListInduction.

Methods

listInductionC Source #

Arguments

:: Proxy c
-> f '[]	case: `SNil`
-> (forall y ys. c y => f ys -> f (y ': ys))	case: `SCons`
-> f xs

Instances

ListInductionC c ([] :: [Type]) Source #
Instance details Defined in Kleene.Type Methods listInductionC :: Proxy c -> f [] -> (forall y (ys :: [Type]). c y => f ys -> f (y ': ys)) -> f [] Source #
(c x, ListInductionC c xs) => ListInductionC c (x ': xs) Source #
Instance details Defined in Kleene.Type Methods listInductionC :: Proxy c -> f [] -> (forall y (ys :: [Type]). c y => f ys -> f (y ': ys)) -> f (x ': xs) Source #

listInductionP Source #

Arguments

:: f '[]	case: `SNil`
-> (forall y ys. f ys -> f (y ': ys))	case: `SCons`
-> SList xs
-> f xs

This is the third variant of list induction, using a proof object SList.

RE structure

class REInductionC (c :: * -> Constraint) (re :: RE *) where Source #

Constrainted RE induction of lists!

We need the Match object, as it connects re and xs.

Note: This is an induction on the structure of the Match, not the xs list.

Methods

reInductionC Source #

Arguments

:: Proxy c
-> f '[]	case: `MatchE`
-> (forall x. c x => f '[x])	case: `MatchV`
-> (forall xs ys. SList xs -> f xs -> f ys -> f (Append xs ys))	case: `MatchA`
-> (forall xs. f xs -> f xs)	case: `MatchL`
-> (forall xs. f xs -> f xs)	case: `MatchR`
-> f '[]	case: `MatchN`
-> (forall xs ys. SList xs -> f xs -> f ys -> f (Append xs ys))	case: `MatchC`
-> (forall xs. SList xs -> f xs)	case: `MatchT`
-> Match re zs	`Match` proof
-> f zs

Instances

REInductionC c (T :: RE Type) Source #
Instance details Defined in Kleene.Type Methods reInductionC :: Proxy c -> f [] -> (forall x. c x => f (x ': [])) -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). f xs -> f xs) -> (forall (xs :: [Type]). f xs -> f xs) -> f [] -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). SList xs -> f xs) -> Match T zs -> f zs Source #
REInductionC c (E :: RE Type) Source #
Instance details Defined in Kleene.Type Methods reInductionC :: Proxy c -> f [] -> (forall x. c x => f (x ': [])) -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). f xs -> f xs) -> (forall (xs :: [Type]). f xs -> f xs) -> f [] -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). SList xs -> f xs) -> Match E zs -> f zs Source #
REInductionC c x => REInductionC c (S x) Source #
Instance details Defined in Kleene.Type Methods reInductionC :: Proxy c -> f [] -> (forall x0. c x0 => f (x0 ': [])) -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). f xs -> f xs) -> (forall (xs :: [Type]). f xs -> f xs) -> f [] -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). SList xs -> f xs) -> Match (S x) zs -> f zs Source #
c x => REInductionC c (V x) Source #
Instance details Defined in Kleene.Type Methods reInductionC :: Proxy c -> f [] -> (forall x0. c x0 => f (x0 ': [])) -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). f xs -> f xs) -> (forall (xs :: [Type]). f xs -> f xs) -> f [] -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). SList xs -> f xs) -> Match (V x) zs -> f zs Source #
(REInductionC c r, REInductionC c s) => REInductionC c (r :\/ s) Source #
Instance details Defined in Kleene.Type Methods reInductionC :: Proxy c -> f [] -> (forall x. c x => f (x ': [])) -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). f xs -> f xs) -> (forall (xs :: [Type]). f xs -> f xs) -> f [] -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). SList xs -> f xs) -> Match (r :\/ s) zs -> f zs Source #
(REInductionC c r, REInductionC c s) => REInductionC c (r :<> s) Source #
Instance details Defined in Kleene.Type Methods reInductionC :: Proxy c -> f [] -> (forall x. c x => f (x ': [])) -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). f xs -> f xs) -> (forall (xs :: [Type]). f xs -> f xs) -> f [] -> (forall (xs :: [Type]) (ys :: [Type]). SList xs -> f xs -> f ys -> f (Append xs ys)) -> (forall (xs :: [Type]). SList xs -> f xs) -> Match (r :<> s) zs -> f zs Source #

reInductionP Source #

Arguments

:: f '[]	case: `MatchE`
-> (forall x. f '[x])	case: `MatchV`
-> (forall xs ys. SList xs -> f xs -> f ys -> f (Append xs ys))	case: `MatchA`
-> (forall xs. f xs -> f xs)	case: `MatchL`
-> (forall xs. f xs -> f xs)	case: `MatchR`
-> f '[]	case: `MatchN`
-> (forall xs ys. SList xs -> f xs -> f ys -> f (Append xs ys))	case: `MatchC`
-> (forall xs. SList xs -> f xs)	case: `MatchT`
-> Match re zs	`Match` proof
-> f zs

Induction using Match.

Conversion to Haskelly types.

haskelly :: Match re xs -> HList xs -> Haskelly re Source #

Convert to haskelly types1

Note: Inverse would require RE singleton, SRE.

type family Haskelly (re :: RE *) :: * where ... Source #

Equations

Haskelly E = ()
Haskelly (V a) = a
Haskelly (a :<> b) = (Haskelly a, Haskelly b)
Haskelly (a :\/ b) = Either (Haskelly a) (Haskelly b)
Haskelly (S a) = [Haskelly a]
Haskelly T = Int

Key

data Key (s :: Symbol) Source #

Keyword, a Proxy kind-specialised to Symbol

>>> Key @"-l"
Key @"foo"

Constructors

Key

Instances

s ~ s' => IsLabel s (Key s') Source #
Instance details Defined in Kleene.Type Methods fromLabel :: Key s' #
Eq (Key s) Source #
Instance details Defined in Kleene.Type Methods (==) :: Key s -> Key s -> Bool # (/=) :: Key s -> Key s -> Bool #
KnownSymbol s => Show (Key s) Source #
Instance details Defined in Kleene.Type Methods showsPrec :: Int -> Key s -> ShowS # show :: Key s -> String # showList :: [Key s] -> ShowS #
KnownSymbol s => ToArg (Key s) Source #	Prepends the `-` character.
Instance details Defined in Kleene.Type.Examples.KleeneSH Methods toArg :: Key s -> Either String String Source #

key :: Key s -> Key s Source #

>>> key #foo
Key @"foo"

keyVal :: KnownSymbol s => Key s -> String Source #

Lenses

Naming convention is simple: r + 3-5 characters.

rval :: Iso (REList (V a)) (REList (V b)) a b Source #

Look into REalue.

rpair :: Iso (REList (a <> b)) (REList (c <> d)) (REList a, REList b) (REList c, REList d) Source #

rfst :: Lens (REList (a <> c)) (REList (b <> c)) (REList a) (REList b) Source #

rsnd :: Lens (REList (c <> a)) (REList (c <> b)) (REList a) (REList b) Source #

rsum :: Iso (REList (a \/ b)) (REList (c \/ d)) (Either (REList a) (REList b)) (Either (REList c) (REList d)) Source #

rleft :: Prism (REList (a \/ c)) (REList (b \/ c)) (REList a) (REList b) Source #

rright :: Prism (REList (c \/ a)) (REList (c \/ b)) (REList a) (REList b) Source #

rstar :: Traversal (REList (S a)) (REList (S b)) (REList a) (REList b) Source #

rnil :: Prism' (REList (S a)) () Source #

rcons :: Prism (REList (S a)) (REList (S b)) (REList a, REList (S a)) (REList b, REList (S b)) Source #

Top

type T = T Source #

matchT :: SListI xs => Match T xs Source #

withTop :: y -> Match T zs -> HList zs -> y Source #