The mono-traversable package uses type level Peano numbers for MinLen
. I can construct them using chained Succ
s:
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?
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)))
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With