Re: [isabelle] Subtyping

Hash: SHA1

On 25/08/11 13:07, John Munroe wrote:
> Thanks so much. It surely has been helpful!
> One thing though: I can't define the datatype "'a + 'b" with
> datatype 'a + 'b = Inl 'a | Inr 'b
> It doesn't seem to like the '+' operator. Is using "datatype ('a,'b)
> sum" the only way? (I see that it doesn't have to be 'sum' but any
> arbitrary name seems to do.)

I don't think you need to define it.  I'm pretty sure everything I said
is true of the built-in sum type.  However, Christian's suggestion of
how it could be defined is useful to help understand how it works.  If
you use the built-in sum type, you can still define is_Inl as Christian
suggested (a way I have little experience with), or you can define it
like this:

definition is_Inl :: "'a + 'b => bool" where
  "is_Inl x == \<exists> a. x = Inl a"

> Also, is the approach of using sum type more appropriate than
> overloading for my application? Would overloading allow the same
> effect to be produced, i.e. defining a function that gives True only
> if the input is of a particular type?

I don't have much experience with overloading, so I might let someone
else answer this.  But their answer might depend on what your intended
application really is --- what do you want to use this for?

Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla -


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