Safe Haskell | None |
---|---|

Language | Haskell2010 |

Type-nat utilities.

We take Peano numbers as base for operations because they make it much easer to prove things to compiler. Their performance does not seem to introduce a problem, because we use nats primarily along with stack which is a linked list with similar performance characteristics.

Many of things we introduce here are covered in `type-natural`

package,
but unfortunatelly it does not work with GHC 8.6 at the moment of writing
this module. We use `Vinyl`

as source of Peano `Nat`

for now.

## Synopsis

- type Peano = Nat
- data Nat
- type family ToPeano (n :: Nat) :: Peano where ...
- type family FromPeano (n :: Peano) :: Nat where ...
- class KnownPeano (n :: Peano) where
- data SingNat (n :: Nat) where
- peanoVal' :: forall n. KnownPeano n => Natural
- peanoValSing :: forall n. KnownPeano n => Sing n -> Natural
- type family Length l :: Peano where ...
- type family At (n :: Peano) s where ...
- type family Drop (n :: Peano) (s :: [k]) :: [k] where ...
- type family Take (n :: Peano) (s :: [k]) :: [k] where ...
- type family IsLongerThan (l :: [k]) (a :: Peano) :: Bool where ...
- type LongerThan l a = IsLongerThan l a ~ 'True
- class (RequireLongerThan' l a, LongerThan l a) => RequireLongerThan (l :: [k]) (a :: Peano)
- type family IsLongerOrSameLength (l :: [k]) (a :: Peano) :: Bool where ...
- type LongerOrSameLength l a = IsLongerOrSameLength l a ~ 'True
- class (RequireLongerOrSameLength' l a, LongerOrSameLength l a) => RequireLongerOrSameLength (l :: [k]) (a :: Peano)
- requireLongerThan :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
- requireLongerOrSameLength :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))

# General

A mere approximation of the natural numbers. And their image as lifted by
`-XDataKinds`

corresponds to the actual natural numbers.

#### Instances

SingI 'Z Source # | |

Defined in Util.Peano | |

RecSubset (Rec :: (k -> Type) -> [k] -> Type) ('[] :: [k]) (ss :: [k]) ('[] :: [Nat]) | |

Defined in Data.Vinyl.Lens type RecSubsetFCtx Rec f # rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f '[] -> g (Rec f '[])) -> Rec f ss -> g (Rec f ss) # rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f '[] # rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f '[] -> Rec f ss -> Rec f ss # | |

(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k -> Type) -> [k] -> Type) (r ': rs :: [k]) (ss :: [k]) (i ': is) | |

Defined in Data.Vinyl.Lens type RecSubsetFCtx Rec f # rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss) # rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs) # rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f (r ': rs) -> Rec f ss -> Rec f ss # | |

(SingI n, KnownPeano n) => SingI ('S n :: Nat) Source # | |

Defined in Util.Peano | |

IndexWitnesses ('[] :: [Nat]) | |

Defined in Data.Vinyl.TypeLevel indexWitnesses :: [Int] # | |

(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) | |

Defined in Data.Vinyl.TypeLevel indexWitnesses :: [Int] # | |

type Sing Source # | |

Defined in Util.Peano |

class KnownPeano (n :: Peano) where Source #

#### Instances

KnownPeano 'Z Source # | |

KnownPeano a => KnownPeano ('S a) Source # | |

peanoVal' :: forall n. KnownPeano n => Natural Source #

peanoValSing :: forall n. KnownPeano n => Sing n -> Natural Source #

Get runtime value from singleton.

# Lists

# Morley-specific utils

type family IsLongerThan (l :: [k]) (a :: Peano) :: Bool where ... Source #

Comparison of type-level naturals, as a function.

It is as lazy on the list argument as possible - there is no need to know the whole list if the natural argument is small enough. This property is important if we want to be able to extract reusable parts of code which are aware only of relevant part of stack.

IsLongerThan (_ ': _) 'Z = 'True | |

IsLongerThan (_ ': xs) ('S a) = IsLongerThan xs a | |

IsLongerThan '[] _ = 'False |

type LongerThan l a = IsLongerThan l a ~ 'True Source #

Comparison of type-level naturals, as a constraint.

class (RequireLongerThan' l a, LongerThan l a) => RequireLongerThan (l :: [k]) (a :: Peano) Source #

#### Instances

(RequireLongerThan' l a, LongerThan l a) => RequireLongerThan (l :: [k]) a Source # | |

Defined in Util.Peano |

type family IsLongerOrSameLength (l :: [k]) (a :: Peano) :: Bool where ... Source #

Similar to `IsLongerThan`

, but returns `True`

when list length
equals to the passed number.

IsLongerOrSameLength _ 'Z = 'True | |

IsLongerOrSameLength (_ ': xs) ('S a) = IsLongerOrSameLength xs a | |

IsLongerOrSameLength '[] ('S _) = 'False |

type LongerOrSameLength l a = IsLongerOrSameLength l a ~ 'True Source #

`IsLongerOrSameLength`

in form of constraint that gives most
information to GHC.

class (RequireLongerOrSameLength' l a, LongerOrSameLength l a) => RequireLongerOrSameLength (l :: [k]) (a :: Peano) Source #

We can have
`RequireLongerOrSameLength = (RequireLongerOrSameLength' l a, LongerOrSameLength l a)`,
but apparently the printed error message can be caused by `LongerOrSameLength`

rather than `RequireLongerOrSameLength`

`.
We do not know for sure how it all works, but we think that if we require constraint X before
Y (using multiple `=>`s) then X will always be evaluated first.

#### Instances

(RequireLongerOrSameLength' l a, LongerOrSameLength l a) => RequireLongerOrSameLength (l :: [k]) a Source # | |

Defined in Util.Peano |

# Length constraints

`Dict`

ionaries

requireLongerThan :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n)) Source #

requireLongerOrSameLength :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n)) Source #