Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data Zero = Zero
- data Succ nat = Succ nat
- class TypeNat nat where
- toValueNat :: Num i => nat -> i
- typeNat :: nat
- type family AddNat x y
- type family MaxNat x y
- data MinLen nat mono
- unMinLen :: MinLen nat mono -> mono
- toMinLenZero :: MonoFoldable mono => mono -> MinLen Zero mono
- toMinLen :: (MonoFoldable mono, TypeNat nat) => mono -> Maybe (MinLen nat mono)
- unsafeToMinLen :: mono -> MinLen nat mono
- mlcons :: IsSequence seq => Element seq -> MinLen nat seq -> MinLen (Succ nat) seq
- mlappend :: IsSequence seq => MinLen x seq -> MinLen y seq -> MinLen (AddNat x y) seq
- mlunion :: GrowingAppend mono => MinLen x mono -> MinLen y mono -> MinLen (MaxNat x y) mono
- head :: MonoFoldable mono => MinLen (Succ nat) mono -> Element mono
- last :: MonoFoldable mono => MinLen (Succ nat) mono -> Element mono
- tailML :: IsSequence seq => MinLen (Succ nat) seq -> MinLen nat seq
- initML :: IsSequence seq => MinLen (Succ nat) seq -> MinLen nat seq
- class (Semigroup mono, MonoFoldable mono) => GrowingAppend mono
- ofoldMap1 :: (MonoFoldable mono, Semigroup m) => (Element mono -> m) -> MinLen (Succ nat) mono -> m
- ofold1 :: (MonoFoldable mono, Semigroup (Element mono)) => MinLen (Succ nat) mono -> Element mono
- ofoldr1 :: MonoFoldable mono => (Element mono -> Element mono -> Element mono) -> MinLen (Succ nat) mono -> Element mono
- ofoldl1' :: MonoFoldable mono => (Element mono -> Element mono -> Element mono) -> MinLen (Succ nat) mono -> Element mono
- maximum :: MonoFoldableOrd mono => MinLen (Succ nat) mono -> Element mono
- minimum :: MonoFoldableOrd mono => MinLen (Succ nat) mono -> Element mono
- maximumBy :: MonoFoldable mono => (Element mono -> Element mono -> Ordering) -> MinLen (Succ nat) mono -> Element mono
- minimumBy :: MonoFoldable mono => (Element mono -> Element mono -> Ordering) -> MinLen (Succ nat) mono -> Element mono
Type level naturals
Peano numbers
Peano numbers are a simple way to
represent natural numbers (0, 1, 2...) using only a Zero
value and a
successor function (Succ
). Each application of Succ
increases the number
by 1, so Succ Zero
is 1, Succ (Succ Zero)
is 2, etc.
data Zero
Zero
is the base value for the Peano numbers.
TypeNat Zero | |
MonoPointed mono => MonoPointed (MinLen (Succ Zero) mono) | |
MonoPointed mono => MonoPointed (MinLen Zero mono) | |
type MaxNat x Zero = x | |
type MaxNat Zero y = y | |
type AddNat Zero y = y |
data Succ nat
Succ
represents the next number in the sequence of natural numbers.
It takes a nat
(a natural number) as an argument.
Zero
is a nat
, allowing
to represent 1.Succ
Zero
Succ
is also a nat
, so it can be applied to itself, allowing
to represent 2,
Succ
(Succ
Zero
)
to represent 3, and so on.Succ
(Succ
(Succ
Zero
))
Succ nat |
class TypeNat nat where
Type-level natural number utility typeclass
toValueNat :: Num i => nat -> i
Turn a type-level natural number into a number
>toValueNat
Zero
0 >toValueNat
(Succ
(Succ
(Succ
Zero
))) 3
typeNat :: nat
type family AddNat x y
type family MaxNat x y
Minimum length data wrapper
data MinLen nat mono
A wrapper around a container which encodes its minimum length in the type system.
This allows functions like head
and maximum
to be made safe without using Maybe
.
The length, nat
, is encoded as a Peano number,
which starts with the Zero
constructor and is made one larger with each application
of Succ
(Zero
for 0,
for 1, Succ
Zero
for 2, etc.).
Functions which require at least one element, then, are typed with Succ
(Succ
Zero
)Succ nat
,
where nat
is either Zero
or any number of applications of Succ
:
head
::MonoTraversable
mono =>MinLen
(Succ
nat) mono ->Element
mono
The length is also a phantom type,
i.e. it is only used on the left hand side of the type and doesn't exist at runtime.
Notice how
isn't included in the printed output:Succ
Zero
>toMinLen
[1,2,3] ::Maybe
(MinLen
(Succ
Zero
) [Int
])Just
(MinLen
{unMinLen = [1,2,3]})
You can still use GHCI's :i
command to see the phantom type information:
> let xs =mlcons
1 $toMinLenZero
[] > :i xs xs ::Num
t =>MinLen
(Succ
Zero
) [t]
Functor (MinLen nat) | |
Eq mono => Eq (MinLen nat mono) | |
(Data nat, Data mono) => Data (MinLen nat mono) | |
Ord mono => Ord (MinLen nat mono) | |
Read mono => Read (MinLen nat mono) | |
Show mono => Show (MinLen nat mono) | |
GrowingAppend mono => Semigroup (MinLen nat mono) | |
MonoPointed mono => MonoPointed (MinLen (Succ Zero) mono) | |
MonoPointed mono => MonoPointed (MinLen Zero mono) | |
MonoTraversable mono => MonoTraversable (MinLen nat mono) | |
MonoFoldableOrd mono => MonoFoldableOrd (MinLen nat mono) | |
MonoFoldable mono => MonoFoldable (MinLen nat mono) | |
MonoFunctor mono => MonoFunctor (MinLen nat mono) | |
GrowingAppend mono => GrowingAppend (MinLen nat mono) | |
SemiSequence seq => SemiSequence (MinLen nat seq) | |
Typeable (* -> * -> *) MinLen | |
type Element (MinLen nat mono) = Element mono | |
type Index (MinLen nat seq) = Index seq |
toMinLenZero :: MonoFoldable mono => mono -> MinLen Zero mono
Types a container as having a minimum length of zero. This is useful when combined with other MinLen
functions that increase the size of the container.
Examples
> > 1 `mlcons`toMinLenZero
[] >MinLen
{unMinLen = [1]}
toMinLen :: (MonoFoldable mono, TypeNat nat) => mono -> Maybe (MinLen nat mono)
unsafeToMinLen :: mono -> MinLen nat mono
Unsafe
Although this function itself cannot cause a segfault, it breaks the
safety guarantees of MinLen
and can lead to a segfault when using
otherwise safe functions.
Examples
> let xs =unsafeToMinLen
[] ::MinLen
(Succ
Zero
) [Int
] >olength
xs 0 >head
xs *** Exception: Data.MonoTraversable.headEx: empty
head :: MonoFoldable mono => MinLen (Succ nat) mono -> Element mono
last :: MonoFoldable mono => MinLen (Succ nat) mono -> Element mono
tailML :: IsSequence seq => MinLen (Succ nat) seq -> MinLen nat seq
initML :: IsSequence seq => MinLen (Succ nat) seq -> MinLen nat seq
class (Semigroup mono, MonoFoldable mono) => GrowingAppend mono
olength (x <> y) >= olength x + olength y
GrowingAppend ByteString | |
GrowingAppend ByteString | |
GrowingAppend IntSet | |
GrowingAppend Text | |
GrowingAppend Text | |
GrowingAppend [a] | |
GrowingAppend (IntMap v) | |
Ord v => GrowingAppend (Set v) | |
GrowingAppend (Seq a) | |
Storable a => GrowingAppend (Vector a) | |
GrowingAppend (NonEmpty a) | |
GrowingAppend (Vector a) | |
(Eq v, Hashable v) => GrowingAppend (HashSet v) | |
Unbox a => GrowingAppend (Vector a) | |
GrowingAppend (DList a) | |
Ord k => GrowingAppend (Map k v) | |
(Eq k, Hashable k) => GrowingAppend (HashMap k v) | |
GrowingAppend mono => GrowingAppend (MinLen nat mono) |
ofoldMap1 :: (MonoFoldable mono, Semigroup m) => (Element mono -> m) -> MinLen (Succ nat) mono -> m
Map each element of a monomorphic container to a semigroup, and combine the results.
Safe version of ofoldMap1Ex
, only works on monomorphic containers wrapped in a
.MinLen
(Succ
nat)
Examples
> let xs = ("hello", 1 ::Integer
) `mlcons` (" world", 2) `mlcons` (toMinLenZero
[]) >ofoldMap1
fst
xs "hello world"
ofold1 :: (MonoFoldable mono, Semigroup (Element mono)) => MinLen (Succ nat) mono -> Element mono
Join a monomorphic container, whose elements are Semigroup
s, together.
Safe, only works on monomorphic containers wrapped in a
.MinLen
(Succ
nat)
Examples
> let xs = "a" `mlcons` "b" `mlcons` "c" `mlcons` (toMinLenZero
[]) > xsMinLen
{unMinLen = ["a","b","c"]} >ofold1
xs "abc"
ofoldr1 :: MonoFoldable mono => (Element mono -> Element mono -> Element mono) -> MinLen (Succ nat) mono -> Element mono
Right-associative fold of a monomorphic container with no base element.
Safe version of ofoldr1Ex
, only works on monomorphic containers wrapped in a
.MinLen
(Succ
nat)
foldr1
f = Prelude.foldr1
f .otoList
Examples
> let xs = "a" `mlcons` "b" `mlcons` "c" `mlcons` (toMinLenZero
[]) >ofoldr1
(++) xs "abc"
ofoldl1' :: MonoFoldable mono => (Element mono -> Element mono -> Element mono) -> MinLen (Succ nat) mono -> Element mono
Strict left-associative fold of a monomorphic container with no base element.
Safe version of ofoldl1Ex'
, only works on monomorphic containers wrapped in a
.MinLen
(Succ
nat)
foldl1'
f = Prelude.foldl1'
f .otoList
Examples
> let xs = "a" `mlcons` "b" `mlcons` "c" `mlcons` (toMinLenZero
[]) >ofoldl1'
(++) xs "abc"
maximum :: MonoFoldableOrd mono => MinLen (Succ nat) mono -> Element mono
minimum :: MonoFoldableOrd mono => MinLen (Succ nat) mono -> Element mono
maximumBy :: MonoFoldable mono => (Element mono -> Element mono -> Ordering) -> MinLen (Succ nat) mono -> Element mono
Get the maximum element of a monomorphic container, using a supplied element ordering function.
Safe version of maximumByEx
, only works on monomorphic containers wrapped in a
.MinLen
(Succ
nat)
minimumBy :: MonoFoldable mono => (Element mono -> Element mono -> Ordering) -> MinLen (Succ nat) mono -> Element mono
Get the minimum element of a monomorphic container, using a supplied element ordering function.
Safe version of minimumByEx
, only works on monomorphic containers wrapped in a
.MinLen
(Succ
nat)