Hi Johannes, hi Andreas,
the core of the problem is that dictionaries are always generated for
type class instances, even if the operations therein are never referred
to. Is this the first time that we have such a situation, or are there
more examples (e.g. in the AFP)? If yes, the code
AFAIK, it is the first time we have such a situation. We have two cases
I'm aware of: "open" in topological_space and "uniformity" in
uniform_space. Up to now we could just remove all code equations from
open as it is a predicate and doesn't produce any problem with the
dictionary construction.
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)
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
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
Okay Fabian and I discovered the following problems when one defines a
type class which contains a constant which is not a function:
1. If there is a type class which contains data depending on the type
classes variable, i.e.
class test_class =
fixes test :: "'a filter"
Hi 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
