[Why3-club] WhyML questions: function without body? polymorphic Sum?

Guillaume Melquiond guillaume.melquiond at inria.fr
Tue Nov 27 18:09:57 CET 2012

Le mardi 27 novembre 2012 à 17:44 +0100, Guillaume Melquiond a écrit :

> >   2. When defining "type container", is there a way to use a
> > polymorphic "continuous_profile_and_location_data", i.e.
> > "continuous_profile_and_location_data 'a"? Right now, I am forced to
> > precise the type 'a to int (as container in sum.Sum is not
> > polymorphic) and thus my function "sum_from_LRBG_before_n" only works
> > with "profile" of type "continuous_profile_and_location_data int". My
> > objective is to get a sum.Sum function that sums
> > "(continuous_profile_and_location_data 'a)[i].cont_distance" elements.
> I don't think it is possible currently. I can't see any kind of issue
> that would be caused by allowing it, so it might just have been some
> shortsightedness when it was implemented; I will let others comment.

I had a discussion with Andrei about it and it appears that, while there
are no theoretical difficulties with such a feature, there are several
technical ones, so it might not happen anytime soon.

For instance, there is an issue with algebraic datatypes. If they happen
to refer to the abstract type you are substituting by a polymorphic
type, then the type variables have to be propagated to the datatype
(e.g., lambda-lifting). But then the order of the variables start to
matter since these types will presumably be used after cloning. So it
means that the user needs a way to control their appearance order. And
so on.

Best regards,


More information about the Why3-club mailing list