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 :: MonoTraversable mono => MinLen (Succ nat) mono -> Element mono
- last :: MonoTraversable 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.
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 |
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 Succ Zero
to represent 1.
Succ
is also a nat
, so it can be applied to itself, allowing Succ (Succ Zero)
to represent 2,
Succ (Succ (Succ Zero))
to represent 3, and so on.
Succ nat |
class TypeNat nat where Source
toValueNat :: Num i => nat -> i Source
Adds two type-level naturals. See the mlappend
type signature for an example.
Calculates the maximum of two type-level naturals. See the mlunion
type signature for an example.
Minimum length newtype wrapper
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, Succ Zero
for 1, Succ (Succ Zero)
for 2, etc.).
Functions which require atleast one element, then, are typed with 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 Succ Zero
isn't included in the printed output:
> 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 = 1 `mlcons` 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 Source
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) Source
Attempts to add a MinLen
constraint to a MonoFoldable
.
Examples
> let xs = toMinLen [1,2,3] :: Maybe (MinLen (Succ Zero) [Int]) > xs Just (MinLen {unMinLen = [1,2,3]}) > :i xs xs :: Maybe (MinLen (Succ Zero) [Int])
> toMinLen [] :: Maybe (MinLen (Succ Zero) [Int]) Nothing
unsafeToMinLen :: mono -> MinLen nat mono Source
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] > length xs 0 > head xs *** Exception: Data.MonoTraversable.headEx: empty
mlcons :: IsSequence seq => Element seq -> MinLen nat seq -> MinLen (Succ nat) seq infixr 5 Source
Adds an element to the front of a list, increasing its minimum length by 1.
Examples
> let xs = unsafeToMinLen [1,2,3] :: MinLen (Succ Zero) [Int] > 0 `mlcons` xs MinLen {unMinLen = [0,1,2,3]}
mlappend :: IsSequence seq => MinLen x seq -> MinLen y seq -> MinLen (AddNat x y) seq Source
Concatenates two sequences, adding their minimum lengths together.
Examples
> let xs = unsafeToMinLen [1,2,3] :: MinLen (Succ Zero) [Int] > xs `mlappend` xs MinLen {unMinLen = [1,2,3,1,2,3]}
mlunion :: GrowingAppend mono => MinLen x mono -> MinLen y mono -> MinLen (MaxNat x y) mono Source
Joins two semigroups, keeping the larger MinLen
of the two.
Examples
> let xs = unsafeToMinLen [1] :: MinLen (Succ Zero) [Int] > let ys = xs `mlunion` xs > ys MinLen {unMinLen = [1,1]} > :i ys ys :: MinLen (Succ Zero) [Int]
head :: MonoTraversable mono => MinLen (Succ nat) mono -> Element mono Source
Returns the first element.
last :: MonoTraversable mono => MinLen (Succ nat) mono -> Element mono Source
Returns the last element.
tailML :: IsSequence seq => MinLen (Succ nat) seq -> MinLen nat seq Source
Returns all but the first element of a sequence, reducing its MinLen
by 1.
Examples
> let xs = toMinLen [1,2,3] :: Maybe (MinLen (Succ Zero) [Int]) > fmap initML xs Just (MinLen {unMinLen = [1,2]})
initML :: IsSequence seq => MinLen (Succ nat) seq -> MinLen nat seq Source
Returns all but the last element of a sequence, reducing its MinLen
by 1.
Examples
> let xs = toMinLen [1,2,3] :: Maybe (MinLen (Succ Zero) [Int]) > fmap initML xs Just (MinLen {unMinLen = [1,2]})
class (Semigroup mono, MonoFoldable mono) => GrowingAppend mono Source
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) | |
(Eq v, Hashable v) => GrowingAppend (HashSet v) | |
GrowingAppend (NonEmpty a) | |
GrowingAppend (Vector a) | |
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 Source
Maps a function that returns a Semigroup
over the container, then joins those semigroups together.
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 Source
Joins a list of Semigroups
together.
Examples
> let xs = "a" `mlcons` "b" `mlcons` "c" `mlcons` (toMinLenZero []) > xs MinLen {unMinLen = ["a","b","c"]} > ofold1 xs "abc"
ofoldr1 :: MonoFoldable mono => (Element mono -> Element mono -> Element mono) -> MinLen (Succ nat) mono -> Element mono Source
ofoldl1' :: MonoFoldable mono => (Element mono -> Element mono -> Element mono) -> MinLen (Succ nat) mono -> Element mono Source
maximum :: MonoFoldableOrd mono => MinLen (Succ nat) mono -> Element mono Source
Like Data.List.maximum
, but not partial on a MonoFoldable.
Examples
> let xs = toMinLen [1,2,3] :: Maybe (MinLen (Succ Zero) [Int]) > fmap maximum xs Just 3
minimum :: MonoFoldableOrd mono => MinLen (Succ nat) mono -> Element mono Source
Like Data.List.minimum
, but not partial on a MonoFoldable.
Examples
> let xs = toMinLen [1,2,3] :: Maybe (MinLen (Succ Zero) [Int]) > fmap minimum xs Just 1