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.

`Zero`

is the base value for the Peano numbers.

TypeNat Zero | |

IsSequence mono => MonoComonad (MinLen (Succ Zero) mono) | For For example, for
Meant to be a direct analogy to the instance for |

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

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 |

TypeNat nat => TypeNat (Succ nat) | |

IsSequence mono => MonoComonad (MinLen (Succ Zero) mono) | For For example, for
Meant to be a direct analogy to the instance for |

MonoPointed mono => MonoPointed (MinLen (Succ Zero) mono) | |

type AddNat (Succ x) y = AddNat x (Succ y) | |

type MaxNat (Succ x) (Succ y) = Succ (MaxNat x y) |

class TypeNat nat where Source

Type-level natural number utility typeclass

toValueNat :: Num i => nat -> i Source

Turn a type-level natural number into a number

>`toValueNat`

`Zero`

0 >`toValueNat`

(`Succ`

(`Succ`

(`Succ`

`Zero`

))) 3

# 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,

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) | |

IsSequence mono => MonoComonad (MinLen (Succ Zero) mono) | For For example, for
Meant to be a direct analogy to the instance for |

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) | |

MonoFoldableEq mono => MonoFoldableEq (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]}

unsafeToMinLen :: mono -> MinLen nat mono Source

**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

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) | |

GrowingAppend (DList a) | |

GrowingAppend (NonEmpty a) | |

(Eq v, Hashable v) => GrowingAppend (HashSet v) | |

GrowingAppend (Vector a) | |

Unbox a => GrowingAppend (Vector a) | |

Storable a => GrowingAppend (Vector 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

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 Source

ofoldr1 :: MonoFoldable mono => (Element mono -> Element mono -> Element mono) -> MinLen (Succ nat) mono -> Element mono Source

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 Source

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"

maximumBy :: MonoFoldable mono => (Element mono -> Element mono -> Ordering) -> MinLen (Succ nat) mono -> Element mono Source

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 Source

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)