Last active
September 6, 2018 14:57
-
-
Save wuct/d32a86b4c32d7cb86278714cf3a4a1da 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
data Zero | |
data Succ n | |
type Two = Succ (Succ Zero) | |
type Three = Succ (Succ (Succ Zero)) | |
data True | |
data False | |
class IsEven n b | |
class IsOdd n b | |
instance isEvenZero :: IsEven Zero True | |
instance isEvenSucc :: IsOdd n b ⇒ IsEven (Succ n) b | |
instance isOddZero :: IsOdd Zero False | |
instance isOddSucc :: IsEven n b ⇒ IsOdd (Succ n) b | |
undefined :: ∀ a. a | |
undefined = unsafeCoerce unit | |
test1 :: True | |
test1 = (undefined :: ∀ b. IsEven Two b => b) | |
-- Can't get compiled | |
-- test2 :: True | |
-- test2 = (undefined :: ∀ b. IsEven Three b => b) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment