Re: [isabelle] Subtyping
-----BEGIN PGP SIGNED MESSAGE-----
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
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?
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
-----END PGP SIGNATURE-----
This archive was generated by a fusion of
Pipermail (Mailman edition) and