Created
September 12, 2018 13:55
-
-
Save acple/7b9cbb836658e79d0ecae313912421fe to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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