Type-level deMorgan laws for kind Bool

Learn
#1

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?

#2

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.

#3

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?

#4

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
#5

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.