Re: [isabelle] Trying to instantiate a class



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.