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