We can use sum to get boolean from two units (1+1=2)
Notation
Rules
Types are defined by their formation, term introduction, term eliminator and computation rules:
Boolean Type |
|||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
formation rule dont really need to have two copies of Unit, just making the point this is a sum. |
|
||||||||||
| term introduction rule |
|
||||||||||
term eliminator assume: a implies c |
|
||||||||||
| computation rule | beta reduction match(inl(a), x.cA y.cB) ->β cA[a/x] match(inr(b), x.cA y.cB) ->β cB[b/x] |
||||||||||
Local completeness rule |
|||||||||||
Unit:Type Idris Code
Idris Code for Boolean is here.
The formation and term introduction rules can be represented simply in Idris like this: |
||| Boolean Data Type data Bool = False | True |
| The term eliminator can be implemented by the if-then-else construct or perhaps, a bit more generally the 'case' construct. | ||| The underlying implementation of the if ... then ... else ... syntax ||| @ b the condition on the if ||| @ t the value if b is true ||| @ e the value if b is false ifThenElse : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a ifThenElse True t e = t ifThenElse False t e = e |
| computation and local completeness rules | if True then True else False if False then False else True |
Negation
We can then add negation
formation rule |
|||
term introduction rule |
|
||
| term eliminator | |||
| computation rule | |||
Local completeness rule |
Bottom Rule
formation rule |
|||
term introduction rule |
|
||
| term eliminator | |||
| computation rule | |||
Local completeness rule |
The formation rule (e.g. Bool : Set)
The introduction rules (e.g. true : Bool and false : Bool)
The elimination rules (e.g. if P : Bool -> Set, b : Bool, pt : P true, and pf : P false, then if b then pt else pf : P b)
The computation rules (e.g. if true then pt else pf = pt and if false then pt else pf = pf)
We can use sum to get boolean from two units (1+1=2)
Boolean Type |
|||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
formation rule dont really need to have two copies of Unit, just making the point this is a sum. |
|
||||||||||
| term introduction rule |
|
||||||||||
term eliminator assume: a implies c |
|
||||||||||
| computation rule | beta reduction match(inl(a), x.cA y.cB) ->β cA[a/x] match(inr(b), x.cA y.cB) ->β cB[b/x] |
||||||||||
Local completeness rule |
|||||||||||
We can then add negation
Negation Rule
formation rule |
|||
term introduction rule |
|
||
| term eliminator | |||
| computation rule | |||
Local completeness rule |
Bottom Rule
formation rule |
|||
term introduction rule |
|
||
| term eliminator | |||
| computation rule | |||
Local completeness rule |
Next Steps
Other types are discussed on the following pages:
