Re: [isabelle] Trying to instantiate a class



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.