Recent versions of base have type families &&
and ||
on kind Bool
.
Can we do type-level logic with them? I’d like to use the facts that &&
and ||
are the categorical product and coproduct on the following
category.
data HomBool (x :: Bool) (y :: Bool) where
Id :: HomBool x x
ExFalso :: HomBool 'False 'True
instance Category HomBool where
id = Id
Id . f = f
f . Id = f
To that end, we would e.g. need to define a homomorphism
homFst :: HomBool (x && y) x
but that seems to require pattern-matching on the type of (x && y)
which (a) type families don’t support, (b) GHC won’t even accept the
type signature because &&
is not injective.
Similar problems arise when considering deMorgan laws for the two type
families. I remember there exist quite complete libraries for type-level
arithmetic theorems. Has anyone implemented theorems for kind Bool
?