Re: [isabelle] Trying to instantiate a class



Thanks for the suggestion. In the end, I wrapped my strings (and other
types) in a datatype. I added some abbreviations and new syntactic
notation which makes this not as bad as I expected. Plus it now feels
like I'm working with Isabelle rather than against it :-)

-Andrew

On Thu, Feb 26, 2015 at 10:56 AM, Viorel Preoteasa
<viorel.preoteasa at aalto.fi> wrote:
> 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.