# Type-level deMorgan laws for kind Bool

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`?

You need some run-time dependency, here is a minimal encoding of singletons so that your function becomes `homFst = homFstVis typeRep typeRep`, with invisible `Typeable` arguments.

``````import Type.Reflection

type Pi :: k -> Type
type Pi = TypeRep

pattern IsFalse :: () => fls ~~ False => Pi fls
pattern IsFalse <- (eqTypeRep (typeRep @False) -> Just HRefl)
where IsFalse = TypeRep

pattern IsTrue :: () => tru ~~ True => Pi tru
pattern IsTrue <- (eqTypeRep (typeRep @True) -> Just HRefl)
where IsTrue = TypeRep

homFstVis :: Pi x -> Pi y -> HomBool (x && y) x
homFstVis IsFalse _       = Id
homFstVis IsTrue  IsTrue  = Id
homFstVis IsTrue  IsFalse = ExFalso
``````

Also look at encoding “function graphs”, see section “3 Slices of Thinnings” of Everybody’s Got To Be Somewhere.

Thanks!
But while ghci correctly checks the type of `homFstVis typeRep typeRep`, I can not define a term using the very same definition and signature. I get ambiguous type variable errors. What have I done wrong?

You would need ScopedTypeVariables (typing from memory)

``````homFst :: forall x y. Typeable x => Typeable y => HomBool (x && y) x
homFst = homFstVis (typeRep @x) (typeRep @y)
``````
1 Like

There are other approches I’m sure. I used `TypeRep` to highlight that it is a singleton type. If you’re not willing to wait for dependent types then you’d use the singletons library instead.