[isabelle-dev] Problem with code generation for non-executable types

[Johannes Hölzl]

Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann:
> Ho Johannes.
> 
> > > >      Then the dictionary construction for type constructors
> > > > does
> > > > not
> > > >      work in ML! The type signature would be the following:
> > > > 
> > > >        val test_prod : ('a * 'b) filter
> > > > 
> > > >      Which apparently is not allow in ML.
> > > This is the famous value restriction (which I also regularly run
> > > into). The standard 
> > > solution is to add a unit closure, because functions may be 
> > > polymorphic in ML.
> 
> Nothing to add about that.
> 
> In the examples there is also the problem that constructing a
> dictionary
> provokes an exception already.  Here the general solution is to hide
> the
> problematic terms beneath an abstraction beneath a constructor.
> 
> Applying that to your examples, I had a look at the sources and came
> to
> the conclusion that it is a bad idea have Abs_filter and Rep_filter
> in
> generated code at all.
> 
> For the simple examples, it is much better to use »principal« as a
> formal constructor, which maps nicely to sets and provides some
> executability for a considerable class of filters.
> 
> I did not have an idea in which algebraic framework »uniformity«
> could
> fit.  Hence I provided a constructor which is a variant of identity
> and
> used that, which makes also the examples involving uniformity
> compileable (but of course not evaluable).
> 
> Maybe you have an idea how this could be improved.

Well filters are mostly non-computable. Actually I would prefer to tell
the code-generator to not generate code for topologies and uniform
spaces at all, as these type classes are carry only non-computable
data.

But of course your implementation looks cleaner, so I changed in
Isabelle df65f5c27c15.

 - Johannes


> Cheers,
> 	Florian
> 
> > 
> > Ah thanks! This explains it.
> > 
> > Unfortunately, in my case the type is fixed in HOL to:
> > 
> >   uniformity :: ('a * 'a) filter  (where 'a :: uniform_space)
> > 
> > And I do not want to change the type signature for code generation.
> > So
> > I will stick to Solution 3.
> > 
> >  - Johannes
> > 
> > 
> > > > 2.  If your type class contains non-computable data, i.e.
> > > > 
> > > >        instantiation bool :: test_class
> > > >        begin
> > > > 
> > > >        definition "test = if P = NP then top else bot"
> > > > 
> > > >        instance proof qed
> > > >        end
> > > > 
> > > >      You get a non-terminating program at the time point when
> > > > the
> > > >      dictionary for bool :: test_class is constructed. When the
> > > >      code equation is hidden with [code del] one gets a
> > > > exception!
> > > > 
> > > > 3.  Our current solution is to introduce code_datatype
> > > > Abs_filter
> > > >      Rep_filter [code del] and define for each uniformity:
> > > > 
> > > >        uniformity = Abs_filter (%P. Code.abort (STR''FAILED'')
> > > > (Rep_filter test P))
> > > > 
> > > >      @Florian: is the an alternative solution?
> > > > 
> > > > 
> > > > - Johannes
> > > > 
> > > > PS: Here is a short, concrete example:
> > > > 
> > > > theory Scratch
> > > >    imports Complex_Main
> > > > begin
> > > > 
> > > > class test_class =
> > > >    fixes test :: "'a filter"
> > > > 
> > > > instantiation prod :: (test_class, test_class) test_class
> > > > begin
> > > > 
> > > > definition [code del]: "test = (test ×⇩F test :: ('a × 'b)
> > > > filter)"
> > > > 
> > > > instance proof qed
> > > > end
> > > > 
> > > > instantiation unit :: test_class
> > > > begin
> > > > 
> > > > definition [code del]:
> > > >    "(test :: unit filter) = bot"
> > > > 
> > > > instance proof qed
> > > > end
> > > > 
> > > > definition "test2 (x::'a::test_class) = (Suc 0)"
> > > > definition "test3 = test2 ((), ())"
> > > > 
> > > > value [code] "test3"
> > > > 
> > > > section ‹Solution›
> > > > 
> > > > code_datatype Abs_filter
> > > > declare [[code abort: Rep_filter]]
> > > > 
> > > > lemma test_Abort: "test = Abs_filter (λP. Code.abort (STR
> > > > ''test'')
> > > > (λx. Rep_filter test P))"
> > > >    unfolding Code.abort_def Rep_filter_inverse ..
> > > > 
> > > > declare test_Abort[where 'a="'a::test_class * 'b ::
> > > > test_class",
> > > > code]
> > > > declare test_Abort[where 'a=unit, code]
> > > > 
> > > > end
> > > > 
> > > > 
> > > > 
> > > > 
> > > > 
> > > > 
> > > > Am Freitag, den 08.01.2016, 09:56 +0100 schrieb Johannes Hölzl:
> > > > > Hi,
> > > > > 
> > > > > I want to introduce uniform spaces in HOL, for this I need to
> > > > > introduce
> > > > > a type class of the form (see the attached bundle):
> > > > > 
> > > > >    class uniformity =
> > > > >      fixes uniformity :: "('a × 'a) filter"
> > > > > 
> > > > > Note that uniformity is a filter and not a function.
> > > > > 
> > > > > which sits between topological spaces and metric spaces, i.e.
> > > > > every
> > > > > metric type is also in the following type classes:
> > > > > 
> > > > >    class open_uniformity = "open" + uniformity +
> > > > >      assumes open_uniformity: "⋀U. open U ⟷ (∀x∈U. eventually
> > > > > (λ(x',
> > > > > y). x' = x ⟶ y ∈ U) uniformity)"
> > > > > 
> > > > >    class uniformity_dist = dist + uniformity +
> > > > >      assumes uniformity_dist: "uniformity = (INF e:{0 <..}.
> > > > > principal
> > > > > {(x, y). dist x y < e})"
> > > > > 
> > > > > Everything works fine until Affinite_Arithmetic, there in
> > > > > Intersection.thy the code generation fails with the following
> > > > > ML
> > > > > error:
> > > > > 
> > > > >    Error: Type mismatch in type constraint.
> > > > >       Value: {uniformity = uniformity_proda} : {uniformity:
> > > > > 'a}
> > > > >       Constraint: ('a * 'b) uniformity
> > > > >       Reason:
> > > > >          Can't unify 'a to (('a * 'b) * ('a * 'b)) filter
> > > > >             (Type variable is free in surrounding scope)
> > > > >    {uniformity = uniformity_proda} : ('a * 'b) uniformity
> > > > >    At (line 1619 of "generated code")
> > > > >    Exception- Fail "Static Errors" raised
> > > > > 
> > > > > I assume this is a strange interaction btw code_abort and the
> > > > > fact
> > > > > that
> > > > > uniformity is a filter (datatype 'a filter = _EMPTY) and not
> > > > > a
> > > > > function.
> > > > > 
> > > > > Does anybody know how to avoid such kind of errors? Do I need
> > > > > to
> > > > > sprinkle more [code del] or code_abort annotations?
> > > > > 
> > > > >   - Johannes
> > > > > 
> > > > > _______________________________________________
> > > > > isabelle-dev mailing list
> > > > > isabelle-dev at in.tum.de
> > > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinf
> > > > > o/is
> > > > > abel
> > > > > le-dev
> > > > _______________________________________________
> > > > isabelle-dev mailing list
> > > > isabelle-dev at in.tum.de
> > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/
> > > > isab
> > > > elle-dev
> > > > 
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> > 
>