Lawvere theories
Haskell Community [Unofficial]
April 17, 2026
By the way, does the GHC type checker know the principle of induction? Say we have
data Peano = Zero | Succ Peano
class Prop (n :: Peano)
Now suppose I have implemented
instance Prop Zero
instance (Prop n) => Prop (Succ n)
Can I then use the universally quantified constraint
forall n. Prop n
in my contexts?
Discussion in the ATmosphere