aQL'Bool

0. Introduction. Our design for working with data makes use of booleans in the type system. These types do not classify any values but instead are used to parameterise other types with statically known information. For example, we would like to determine statically whether or not two types are equal.

In a dependently typed language, we could work with Bool s directly, as type constructors can have as parameters nontype values. In Haskell, however, such parameters must be first-order types. Hence the functions in this module provide a framework for working with booleans in the Haskell type system.

Some day dependently-typed languages will be commonplace and the manipulations of the present module will be unnecessary. Until that day dawns, though, we have to fake the future.

This module has a simple structure.

{-# LINE 22 "aQL'Bool.hweb" #-}
Pragmas
module AQL'Bool where
Definitions

1. First we define a new second-order type, TBool , inhabited by the booleans.

Definitions:

{-# LINE 29 "aQL'Bool.hweb" #-}
{- data1 TBool = TTrue | TFalse -}
class TBool b
data TTrue; instance TBool TTrue; ttrue = undefined :: TTrue
data TFalse; instance TBool TFalse; tfalse = undefined :: TFalse

instance Show TTrue where show _ = "TTrue"
instance Show TFalse where show _ = "TFalse"

2. It is easy to implement disjunction and conjunction.

Definitions:

 {-# LINE 39 "aQL'Bool.hweb" #-}
{- compute a \/ b -}
class (TBool a, TBool b) => Disj a b where
  type a :\/: b :: *
  (.\/.) :: a -> b -> a :\/: b
  
instance Disj TTrue TTrue where 
  type TTrue:\/: TTrue = TTrue
  _ .\/. _ = ttrue
  
instance Disj TTrue TFalse where 
  type TTrue:\/: TFalse = TTrue
  _ .\/. _ = ttrue
  
instance Disj TFalse TTrue where 
  type TFalse :\/: TTrue = TTrue
  _ .\/. _ = ttrue
  
instance Disj TFalse TFalse where 
  type TFalse :\/: TFalse = TFalse
  _ .\/. _ = tfalse

{- compute a /\ b -}
class (TBool a, TBool b) => Conj a b where
  type a :/\: b :: *
  (./\.) :: a -> b -> a :/\: b
  
instance Conj TTrue TTrue where 
  type TTrue :/\: TTrue = TTrue
  _ ./\. _ = ttrue
  
instance Conj TTrue TFalse where 
  type TTrue:/\: TFalse = TFalse
  _ ./\. _ = tfalse
  
instance Conj TFalse TTrue where 
  type TFalse :/\: TTrue = TFalse
  _ ./\. _ = tfalse
  
instance Conj TFalse TFalse where 
  type TFalse :/\: TFalse = TFalse
  _ ./\. _ = tfalse

3. The conditional is even easier.

Definitions:

{-# LINE 83 "aQL'Bool.hweb" #-}
class TBool b => If'then'else_ b x y where
  type If'then'else b x y :: *
  if'then'else :: b -> x -> y -> If'then'else b x y
  
instance If'then'else_ TTrue x y where
  type If'then'else TTrue x y = x
  if'then'else _ x _ = x
  
instance If'then'else_ TFalse x y where
  type If'then'else TFalse x y = y
  if'then'else _ _ y = y
  
data l :^ v =  l :^ v

4. Needed language extensions.

Pragmas:

{-# LINE 85 "aQL'Bool.hweb" #-}
{-# LANGUAGE 
  TypeFamilies,
  TypeOperators,
  MultiParamTypeClasses,
  FunctionalDependencies, 
  EmptyDataDecls, 
  FlexibleInstances,
  FlexibleContexts,  
  UndecidableInstances,
  TypeSynonymInstances  #-}

5. Names of the sections.
Definitions
Pragmas