Skip to content

Instantly share code, notes, and snippets.

@acple acple/Nat.purs
Created Sep 12, 2018

Embed
What would you like to do?
module Data.Typelevel.Nat where
import Prelude
import Data.Symbol (SProxy(..))
import Prim.Symbol as Symbol
class IsNat nat where
reflectNat :: SProxy nat -> Int
instance nat0 :: IsNat "0" where
reflectNat _ = 0
else
instance nat1 :: IsNat "1" where
reflectNat _ = 1
else
instance nat2 :: IsNat "2" where
reflectNat _ = 2
else
instance nat3 :: IsNat "3" where
reflectNat _ = 3
else
instance nat4 :: IsNat "4" where
reflectNat _ = 4
else
instance nat5 :: IsNat "5" where
reflectNat _ = 5
else
instance nat6 :: IsNat "6" where
reflectNat _ = 6
else
instance nat7 :: IsNat "7" where
reflectNat _ = 7
else
instance nat8 :: IsNat "8" where
reflectNat _ = 8
else
instance nat9 :: IsNat "9" where
reflectNat _ = 9
else
instance nat' ::
( Symbol.Cons head tail nat
, NatConcat head tail
) => IsNat nat where
reflectNat _ = reflectNat' (SProxy :: SProxy head) (SProxy :: SProxy tail) 0
class NatConcat head tail where
reflectNat' :: SProxy head -> SProxy tail -> Int -> Int
instance natConcatNil ::
( IsNat head
) => NatConcat head "" where
reflectNat' head _ = (_ + reflectNat head)
else
instance natConcatCons ::
( Symbol.Cons head' tail' tail
, NatConcat head' tail'
, IsNat head
) => NatConcat head tail where
reflectNat' head _ = reflectNat' (SProxy :: SProxy head') (SProxy :: SProxy tail') <<< (_ * 10) <<< (_ + reflectNat head)
----------------------------------------------------------------
-- repl:
-- > reflectNat (SProxy :: SProxy "123456")
-- 123456
-- > reflectNat (SProxy :: SProxy "1")
-- 1
-- > reflectNat (SProxy :: SProxy "0")
-- 0
-- > reflectNat (SProxy :: SProxy "91")
-- 91
-- > reflectNat (SProxy :: SProxy "123a")
-- Err
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.