Lawvere theories

ashokkimmel:

type Stuck :: Peano
type family Stuck where

This is an irreducible type family, but it’s still technically valid. It also is not an instance of Prop.

Interesting. Is that the type-level equivalent to a function declaration without a function body? Does the kind Peano also contain an infinity type like infinity = Succ infinity? Apparently under UndecidableInstances one can write such a type family. Your Stuck example is more unnerving, though, because it does not require an obviously dangerous language extension. Thanks for showing it!