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 Data.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 ...
- data SingNat (n :: Nat) where
- type family Decrement (a :: Peano) :: Peano where ...
- type family (x :: Peano) > (y :: Peano) :: Bool where ...
- peanoSing :: forall (n :: Nat). SingI (ToPeano n) => SingNat (ToPeano n)
- type family (x :: Peano) >= (y :: Peano) :: Bool where ...
- peanoSingDecrement :: Sing n -> Maybe (Sing (Decrement n))
- 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))
- isGreaterThan :: Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))
- isGreaterEqualThan :: Sing a -> Sing b -> Maybe (Dict ((a >= b) ~ 'True))
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 Morley.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 => SingI ('S n :: Nat) Source # | |
Defined in Morley.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 Morley.Util.Peano |
peanoSing :: forall (n :: Nat). SingI (ToPeano n) => SingNat (ToPeano n) Source #
Get the peano singleton for a given type-level nat literal.
>>>
peanoSing @2
SS (SS SZ)
Peano Arithmetic
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 Morley.Util.Peano | |
MockableConstraint (RequireLongerThan l a) Source # | |
Defined in Morley.Util.Peano unsafeProvideConstraint :: Dict (RequireLongerThan l a) Source # |
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 Morley.Util.Peano | |
MockableConstraint (RequireLongerOrSameLength l a) Source # | |
Defined in Morley.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 #