Re: [isabelle] Non-idempotence of datatype constructors



Hello,

we're talking about Isabelle datatypes here, which are always finite
(final algebras is the categorial interpretation). The Haskell
interpretation is actually a codatatype (the final coalgebra) and
calling them "datatypes" is, in my opinion, actually a bit non-standard.
But it makes sense given the lazy semantics of Haskell.

Manuel


On 01/05/2020 12:59, Andrew Butterfield wrote:
> Hi Manuel,
> 
> it depends on how you interpret a datatype declaration
> 
> In Haskell, the data type
> 
> List = Null | Cons Int List
> 
> is interpreted as defining an "arrow"  List ->  Null +  Cons (Int,List)
> 
> This admits infinite structures and supports laziness in that language
> 
> So the the following Haskell definition is fine
> 
> one = Cons 1 one
> 
> and is implemented with a loop from the one component to the Cons.
> 
> Those more used to the ML flavour of FP will interpret the above datatype as
> 
> Null -> List   and  (Int,List) -> List
> 
> This allows only finite structures, and here it is not possible to
> define 'ones' as above.
> 
> 
>> On 1 May 2020, at 11:24, Manuel Eberl <eberlm at in.tum.de
>> <mailto:eberlm at in.tum.de>> wrote:
>>
>> This is one for our datatype experts:
>>
>> I just noticed that theorems like
>>
>> Cons x xs ≠ xs
>>
>> are not automatically provided by the datatype package although they
>> should clearly hold for any datatype. To be more precise, I am talking
>> about theorems of the form
>>
>> C x1 … xn ≠ x1
>> …
>> C x1 … xn ≠ xn
>>
>> for any n-ary datatype constructor C (and of course also the flipped
>> variant).
>>
>> I'm not sure how useful something like this is in practice and it's
>> fairly easy to prove these by hand when needed. I just ran into a
>> situation where I had an assumption of the form "C a b ≠ b" and was
>> surprised that the simplifier didn't take care of it automatically.
>>
>> I realise that the datatype package already provides an absurd number of
>> theorems and one should be careful to blow it up even more, but seeing
>> as the number of theorems to be generated is linear in the number of
>> constructors and they're probably very easy to prove, one could consider
>> it. Or perhaps at least as an optional plugin or standalone tool.
>>
>> Manuel
>>
>>
>>
> 
> --------------------------------------------------------------------
> Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
> Lero@TCD, Head of Software Foundations & Verification Research Group
> School of Computer Science and Statistics,
> Room G.39, O'Reilly Institute, Trinity College, University of Dublin
>                          http://www.scss.tcd.ie/Andrew.Butterfield/
> --------------------------------------------------------------------
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.