Re: [isabelle] Trying to instantiate a class



Hi Andrew,

There are two ways that approximate what you want.

1. You can define swap at different types using the unrestricted overloading feature (see section 5.9 in the Isar reference manual). The types from the various definitions must not overlap, so you cannot define it on 'a list and strings separately. Type inference does not check that all occurrences of swap in a term have a type that is covered by some definition. Depending on your usage, you might end up with a lot of type annotations, but you can in principle use swap with abstract types. Moreover, code generation does not work for swap. Here's an example:

consts swap :: "string â string â 'a â 'a"

overloading swap_string â "swap :: string â string â char list â char list" begin
definition "swap_string = (undefined :: string â string â char list â char list)"
end

2. Use the package for adhoc overloading (section 11.9 in isar-ref, theory ~~/src/Tools/Adhoc_Overloading). You declare swap as a constant without definition, and a separate constant for every type you need. During type inference, occurrences of swap are replaced by one of the separate constants according on the type. Type checking ensures that there is a unique definition for every occurrence. Thus, you cannot use swap with an abstract type, but code generation works as expected. With a little trick, you can even have generic implementations for type constructors and specialised ones taking precedence. Here's an example:

consts swap :: "string â string â 'a â 'a"

definition swap_string :: "string â string â string â string"
where "swap_string = undefined"

adhoc_overloading swap swap_string

class swap_list

definition swap_list :: "string â string â 'a :: swap_list list â 'a list"
where "swap_list = undefined"

adhoc_overloading swap swap_list

instance int :: swap_list ..

lemma "swap = (swap_list :: _ â _ â int list â _)" ..
lemma "swap = swap_string" ..

You have to instantiate the type class swap_list for all types that you want to use the generic implementation from list. Since the type of the function swap_list is restricted to lists over a type that inhabits the class swap_list, type inference will use swap_string for "char list" (= "string") and swap_list for other types such as "int list".

You cannot use this trick with such a marker type class in the first approach because you could later on instantiate char and thus create inconcistencies. Since the kernel of Isabelle only sees the replaced constants swap_list, swap_string, etc., soundness is not a problem.

Hope this helps,
Andreas


On 25/02/15 17:33, Andrew Gacek wrote:
Let me step back and say that what I primarily want is a way to define
a function at multiple different types so that I can use it with the
same syntax in each case. Originally I did this just by using the same
syntactic abbreviation for all of them, but the number of ambiguous
parses grows way too much.

I want something like

   swap :: string => string => 'a => 'a

which I will define at various types like string, exp, equation, exp
list, string list, string => nat, etc. It would also be nice if the
cases for exp list and string list were derived from a general pattern
for list.

I've tried using locales just now, but I don't think it provides what
I'm looking for (or perhaps I'm using them wrong). If that's right,
then it seems the only solution would be to wrap types like string and
string => nat into datatypes so that I can instantiate a type class in
an ad-hoc fashion for them. The downside is that having something like
string => nat wrapped in a datatype makes the it more cumbersome to
use since I can no longer just apply it to a string to get back a nat.

Is this an accurate assessment?

Thanks,
Andrew


On Wed, Feb 25, 2015 at 9:57 AM, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> wrote:
Hi Andrew,

You can instantiate a type class only for a type constructor such as "list",
not for compound types such as "char list". Since "string" is a type synonym
of "char list", the type class instantiation for "string" must match the
instantiation for "char list". If "char list" and "string" must have
different instantiations, then you have to use some other type constructor
that is isomorphic to string, and do the instantiation for it.

Note that the type "String.literal"  from theory String is such a copy, but
I recommend that you do not use this type copy for your purposes.
String.literal has a specific purpose for code generation, so if you ever
want to generate code (especially in Haskell), you will run into problems
with String.literal.

Hope this helps,
Andreas


On 25/02/15 16:42, Andrew Gacek wrote:

I have a class defined as

class foo =
    fixes foo :: 'a

and I am trying to instantiate it over the type "string" but I get an
error:

instantiation "string" :: foo
Bad type name: "String.string"

Knowing that string is "char list" I tried that instead, but still got an
error:

instantiation "char list" :: foo
Undefined type name: "char list"

Is there any way to instantiate the class over the type "string" like I
want?

I know I could try to instantiate at "char" and then do something
general for "list", but it turns out the definitions I want for the
type "char list" are not the same as doing this for char and then
lifting it to lists.

Perhaps I have to wrap "string" in a datatype to get what I want?

Thanks,
Andrew






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