inv.hs

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, FlexibleInstances, EmptyDataDecls #-}

data Z
data S a
__ = __

data T
data F

class EqNat a b c | a b -> c
instance EqNat Z Z T
instance EqNat (S a) Z F
instance EqNat Z (S b) F
instance EqNat a b c => EqNat (S a) (S b) c

class Add a b c | a b -> c
instance Add Z a a
instance Add a b c => Add (S a) b (S c)
add :: Add a b c => a -> b -> c
add = __

class NLE x y
instance Add x a y => NLE x y

class Mul a b c | a b -> c
instance Mul Z b Z
instance (Mul a b c', Add c' b c) => Mul (S a) b c

class Registry clas a b c | clas a b -> c

class Inv clas init limit a b c | clas init a b -> c
instance (NLE x limit, Registry clas x b a', EqNat a' a r, Inv' r clas x limit a b c) => Inv clas x limit a b c
class Inv' r clas x limit a b c | r clas x a b -> c
instance Inv' T clas x limit a b x
instance Inv clas (S x) limit a b c => Inv' F clas x limit a b c

class FactF a b | a -> b
instance FactF Z (S Z)
instance (FactF a b', Mul (S a) b' b) => FactF (S a) b
factF :: FactF a b => a -> b
factF = __
data RegFact
instance FactF a c => Registry RegFact a b c

class FactR a c | a -> c
instance Inv RegFact (S Z) a a Z c => FactR a c
factR :: FactR a c => a -> c
factR = __

class Fact a b | a -> b, b -> a
instance (FactF a b, FactR b a) => Fact a b
fact :: Fact a b => a -> b
fact = __

four = __ :: S (S (S (S Z)))

n24 = factF four -- inferred: 24
n4 = factR n24 -- inferred: 4
foo = \x -> (fact x `asTypeOf` n24) -- inferred: 4 -> 24

-- bar = \x -> (fact x `asTypeOf` n4) -- compile error