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

[Thorsten Altenkirch]

On 15 Oct 2010, at 09:12, Andreas Abel wrote:

> 
> 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.

but we can use EmptyRec :-)

module emptyRec where

record EmptyRec : Set where
 field
   bla : EmptyRec

Recursive records forever!

Cheers,
Thorsten



> 
> 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/
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda