Geek Answers Handbook

Is there a convenient way to build large numbers like Peano using a monojunction?

The monoprocessor package uses Peano type type numbers for MinLen. I can build them using Succs chain :

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

but it quickly gets out of hand:

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

Is there a convenient way to build large Peano numbers? I see that the GHC has a TypeLiterals extension, but I'm not sure if I can use it here. As an alternative, I can make synonyms like:

type One = Succ Zero
type Two = Succ One

etc.; Does something like this already exist somewhere?

+4
source share
3 answers

TypeLits . , .

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

import qualified GHC.TypeLits as TL

data Nat = Zero | Succ Nat

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

, :

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

Lit n, Nat. GHCi:

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

: type-level. , . , .

UndecidableInstances, . - ( , naturals, DataKinds, * Nat, , 'Succ 'Zero Succ Zero - ):

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

-

Decimal '[One, Two, Five]

125.

+2

You can port type-natural QuasiQuoters .

0
source

More articles:


All Articles