[Agda] Newbie questions after reading Dependently Typed Programming in Agda

[Andreas Abel]

On Oct 14, 2010, at 10:42 PM, Oscar Finnsson wrote:
>     There is no way to define False using records.
>
> Why not? Something to do with type theory (from now on I'll just  
> refer to type theory whenever I don't understand something :) )? If  
> defining True using record is such a good idea why isn't defining  
> False using record a good idea?
> ___________

False needs to be an empty type.  For instance the data type with no  
constructors.  A record type has by definition exactly one  
constructor.  Even if a record type has no fields, it is not empty.   
It is then the nullary cartesian product, or the unit type, with  
exactly one inhabitant.

Of course you can define an empty record type if you already have an  
empty type "Empty".

record EmptyRec : Set where
   field
     bla : Empty

This, obviously, does not provide you with the first empty type who  
ever wandered on earth.

Cheers,
Andreas

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/