Re: [isabelle] Trying to instantiate a class



Hi Andrew,

Why don't you do it like this:

class foo =
  fixes foo :: 'a

instantiation "list" :: (type) foo
  begin
    instance proof qed
  end

You create the instantiation for every kind of lists.
The problem is that instead of char you have an
arbitrary type. If you use some operations on
chars, then this is too abstract, but if you only
work with operations on lists, then this should be
enough.

If you need operations on char in the instantiation,
then you can create another class

class my_char =
  fixes "operations on char that you need to abstract"
  assumes "properties of the operation on char that you need in the list
:: (type) foo instantiation"

Then you create an instantiation of char as my_char:

class my_char =
  fixes my_op :: 'a

class foo_str =
  fixes foo_str :: "'a â 'a"
  assumes foo_rule: "foo_str x = foo_str y"

instantiation "char" :: my_char
  begin
    definition "my_op = CHR ''a''"
    instance proof qed
  end

instantiation "list" :: (my_char) foo_str
  begin
    definition foo_my_char_def: "foo_str x = [my_op]"
    instance proof qed (simp add: foo_my_char_def)
  end

  lemma "foo_str (x::string) = foo_str y"
    by (rule foo_rule)

This gives you the full power as you would get if
it would be possible to instantiate string as foo.
The drawback is that you need to duplicate in
my_char the operations on characters. You can
do it easily by  assuming a bijective function between
my_char and char.

I needed something similar. In my case I needed
to instantiate (nat => 'a::SomeClass) as SomeClass, but it
was not possible, so I created a class Nat, and
I instantiated nat as Nat, and I created the
instance ('a::Nat => 'b::SomeClass) of SomeClass.

You can see the details of this in the archive of formal proofs:

http://afp.sourceforge.net/entries/RefinementReactive.shtml

in the file Temporal.thy

Best regards,

Viorel

On 02/25/2015 07:12 PM, Andreas Lochbihler wrote:
> 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:
>>>>
>>>>

>>>> 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.