Re: [isabelle] Code generation with type classes leads to compile error



Hi Dominique,

> I ran into a case where the code generation produces invalid ML code
> (with the default code generator setup).
> 
> The problem seems to be related to ML code for type classes which under
> certain circumstances leads to a polymorphic value (instead of a
> polymorphic function) for representation of the type class. And
> polymorphic values aren't really polymorphic in ML. The attached theory
> shows this. (Tested with 2019-RC0)
> 
> It gives an error as follows:
> 
> 
>    Error: Type mismatch in type constraint.
>        Value: {uniformity = uniformity_lista} : {uniformity: 'a}
>        Constraint: 'a list uniformity
>        Reason:
>           Can't unify 'a to ('a list * 'a list) filter
>              (Type variable is free in surrounding scope)
>    {uniformity = uniformity_lista} : 'a list uniformity
>    At (line 15 of "generated code")
>    Exception- Fail "Static Errors" raised
> 
> How can I change my code setup so that the code compiles? (Without
> changing the class hierarchy.)

there are some borderline cases in code generation which do not work out
of the box indeed.  Your example involving filters is problematic since
filters are not executable in general at all, so resolving the
dictionary issue won't help.  Do you have a less synthetic example at hand?

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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