Is there a convenient way to construct larger type level Peano numbers using mono-traversable?

Question

The mono-traversable package uses type level Peano numbers for MinLen. I can construct them using chained Succs:

toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ Zero)) [Int])

but this quickly gets out of hand:

toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ (Succ (Succ (Succ Zero))))) [Int])

Is there a convenient way to construct larger Peano numbers? I see GHC has a TypeLiterals extension but I'm not sure if I can use it here. Alternatively, I can make synonyms like:

type One = Succ Zero
type Two = Succ One

and so on; does something like that already exist somewhere?

Answer 1

TypeLits is perfectly good for type-level numerals. Also, it's easy to use it only for syntactic sugar and leave the underlying library-specific implementation unchanged.

{-# LANGUAGE
  UndecidableInstances, TypeFamilies,
  DataKinds, TypeOperators #-}

import qualified GHC.TypeLits as TL

data Nat = Zero | Succ Nat

newtype MinLen (n :: Nat) a = MinLen a

We have to define a type family that converts a literal to the number type:

type family Lit (n :: TL.Nat) :: Nat where
  Lit 0 = Zero
  Lit n = Succ (Lit (n TL.- 1))

Now you can use Lit n whenever you need a Nat literal. In GHCi:

>:kind! MinLen (Lit 3)
MinLen (Lit 3) :: * -> *
= MinLen ('Succ ('Succ ('Succ 'Zero)))

Answer 2

There is a package for this sort of thing: type-level. It's a bit intimidating, and I haven't really explored it yet. But you shouldn't need that much power, so you can roll your own simple bits.

If you're willing to use UndecidableInstances, things are pretty easy. Something approximately like this (I don't know exactly how the naturals are defined in that library; if it doesn't use DataKinds, you may have to use the * kind instead of the Nat kind, and you may have to write 'Succ and 'Zero instead of Succ and Zero--I'm not too clear on that aspect):

{-# LANGUAGE UndecidableInstances, TypeFamilies, DataKinds, TypeOperators #-}

module TAR where

-- You wouldn't actually use this line, because the library
-- provides the naturals
data Nat = Zero | Succ Nat

-- Digits and Ten to get things started
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four
type Six = Succ Five
type Seven = Succ Six
type Eight = Succ Seven
type Nine = Succ Eight
type Ten = Succ Nine

type family Plus (a::Nat) (b::Nat) where
  Plus Zero n = n
  Plus (Succ m) n = Plus m (Succ n)

type family Times (a::Nat) (b::Nat) where
  Times Zero n = Zero
  Times (Succ m) n = Plus n (Times m n)

type Decimal (a::[Nat]) = Decimal' a Zero

type family Decimal' (a::[Nat]) (n::Nat) where
  Decimal' '[] n = n
  Decimal' (a ': bs) n = Decimal' bs (Plus a (Times Ten n))

Then you can write something like

Decimal '[One, Two, Five]

to mean 125.