| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Util.Peano
Description
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 Associated Types type RecSubsetFCtx Rec f # Methods 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 Associated Types type RecSubsetFCtx Rec f # Methods 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 Methods indexWitnesses :: [Int] # | |
| (IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) | |
Defined in Data.Vinyl.TypeLevel Methods 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.
Equations
| 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.
Equations
| 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 Dictionaries
requireLongerThan :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n)) Source #
requireLongerOrSameLength :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n)) Source #