[isabelle-dev] Tweak Haskell output for future Haskell compatibility.

[Christian Sternagel]

Hi all,

recently I thought about something which is slightly related to giving 
sort constraints for datatypes (but also raised a completely unrelated 
question). Let me just give my idea:

Currently I am working on a formalization of Kruskal's Tree Theorem (but 
I am still far from finished ;)) which shows that when a set A is 
well-quasi-ordered (wqo), then the set of finite trees over A is wqo.

Since the strict part of any wqo is well-founded, they can be employed 
in termination analysis.

Moreover, every datatype represents (somehow) a set of finite trees.

So if the type parameters of a datatype are restricted to wqo, we have 
that values of this datatype are wqo. (I guess, also here, as Tobias 
suggested, you can first use an unconstrained datatype and later on add 
the constraints by hand; but I was thinking about something like 
"deriving" in Haskell, where we automatically obtain an instance.)

Now to the unrelated question this raised (maybe "the transfer guys" 
could comment): What would be the best way to prove something about 
"finite trees" (like Kruskal's Tree Theorem) and then obtain this result 
for other finite trees (like every datatype) "for free".

Before I heard about the transfer machinery I thought of axiomatizing 
what it means to be a finite tree in a locale and do the proof inside 
this locale (but this seems a bit cumbersome). Is there any chance that 
having a proof for, lets say

datatype 'a tree = Empty | Node 'a "'a tree list"

to obtain the same result "for free" for any other datatype (as long as 
this proof only depends on the property "being a finite tree").

If this all would work out, maybe wqo could be incorporated (in addition 
to the existing measures) into Isabelle's termination checker (at least 
something similar to primrec is conceivable, where we check for 
tree-embedding of arguments).

As I said, this is just a recent idea (which may contain several flaws).

cheers

chris

On 05/09/2012 01:43 AM, Tobias Nipkow wrote:
> Am 08/05/2012 14:44, schrieb Makarius:
>> So apart from the observation that the foundational kernel does not require sort
>> constraints (apart from HOL.type of course), were there any reasons against them?
>
> They are not allowed in Haskell anymore, so why do we allow them (and complicate
> the code generation for Haskell in the future)? That was the starting point.
>
> That the kernel does not require sort constraints is not the point. Even if it
> did, you would still not need sort constraints in datatypes because their
> construction does not involve any sorts. You could always (I think) define an
> unconstrained datatype, even if its intended usage is in a constrained setting.
>
> I now see that there are certain extra-logical uses and accept that some people
> just like to explicitly constrain the usage of a datatype.
>
> Now that the machinery works smoothly, I would not suggest to remove it.
>
> Tobias
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev