SHARE
TWEET

GCD fun

edv Aug 14th, 2013 30 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
  2. module Test where
  3.  
  4. data Zero
  5. data Succ n
  6.  
  7. type One = Succ Zero
  8. type Two = Succ One
  9. type Four = Succ (Succ Two)
  10. type Six = Succ (Succ Four)
  11. type Eight = Succ (Succ Six)
  12.  
  13. class Nat n where
  14.   toInt :: n -> Int
  15.  
  16. instance Nat Zero where
  17.   toInt _ = 0
  18.  
  19. instance (Nat n) => Nat (Succ n) where
  20.   toInt _ = 1 + toInt (undefined::n)
  21.  
  22. type family GCD d m n
  23. type instance GCD d Zero Zero = d
  24. type instance GCD d (Succ m) (Succ n) = GCD (Succ d) m n
  25. type instance GCD Zero (Succ m) Zero = Succ m
  26. type instance GCD (Succ d) (Succ m) Zero = GCD (Succ Zero) d m
  27. type instance GCD Zero Zero (Succ n) = Succ n
  28. type instance GCD (Succ d) Zero (Succ n) = GCD (Succ Zero) d n
  29.  
  30. fun :: (Nat a, GCD Zero a Four ~ Four) => a -> Int
  31. fun a = toInt a
RAW Paste Data
Pastebin PRO Summer Special!
Get 40% OFF on Pastebin PRO accounts!
Top