Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Subtyping

Email Gateway (Aug 18 2022 at 18:14):

From: John Munroe <munddr@gmail.com>
Hi,

I'm trying to define a function 'f' such that when the input is of
type 'A' it gives true, but when it's of type 'B' it gives false:
Would I need to make A and B subtypes of some parent type, say, 'P',
and that 'f' is of type "P => bool"? I can't seem to find much
documentation on subtyping.

If I use type classes instead:

class P
classes A < P
B < P

I can't seem to define the type of 'f' in terms of neither A, B, or P.

Any help on this will be much appreciated!

Thanks

John

Email Gateway (Aug 18 2022 at 18:14):

From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

It sounds like you might want to use a sum type, so that the type "'p"
is "'a + 'b". There was a discussion about this quite recently on this
very list, starting here: http://tinyurl.com/3jzx3ny

Then you could have something like "f p = \<exists> a. p = Inl a" (but I
haven't tested this).

Tim
<><
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk5UZHMACgkQ/cBxZIxl6rmwnACfdWxXr+HPTl/8EOuAg0Y6j1Ai
378An1HvQucFMwMdkCUv4a+PtWuAXzbO
=Z7Ie
-----END PGP SIGNATURE-----

Email Gateway (Aug 18 2022 at 18:14):

From: John Munroe <munddr@gmail.com>

On 24/08/11 11:03, John Munroe wrote:

Hi,

I'm trying to define a function 'f' such that when the input is of
type 'A' it gives true, but when it's of type 'B' it gives false:
Would I need to make A and B subtypes of some parent type, say, 'P',
and that 'f' is of type "P => bool"? I can't seem to find much
documentation on subtyping.

It sounds like you might want to use a sum type, so that the type "'p"
is "'a + 'b".  There was a discussion about this quite recently on this
very list, starting here: http://tinyurl.com/3jzx3ny

Then you could have something like "f p = \<exists> a. p = Inl a" (but I
haven't tested this).

Thanks for that. I'm not certain if I properly understand "f p =
\<exists> a. p = Inl a". So, for my example, is the type of f "A + B
=> bool"? This is what I have:

typedecl A
typedecl B

axiomatization
f :: "A + B => bool"
where
ax1 : "f p = (EX a. p = Inl a)"

consts a :: "A + 'b"

lemma "f a = True"
apply (simp add: ax1)
??

I can't seem to find out what Inl actually does. It's defined in
Sum_Type to be "Inl = Abs_sum \<circ> Inl_Rep", but I can't seem to
find where Abs_sum is defined.

Thanks

John

Tim
<><
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk5UZHMACgkQ/cBxZIxl6rmwnACfdWxXr+HPTl/8EOuAg0Y6j1Ai
378An1HvQucFMwMdkCUv4a+PtWuAXzbO
=Z7Ie
-----END PGP SIGNATURE-----

Email Gateway (Aug 18 2022 at 18:14):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
(sorry for multiple copies)
Hi there,

I would refrain from going into the "implementation" level of the sum
type (Abs_sum, Inl_rep) and just use pattern matching.

The type A + B represents a type that incorporates values of type A
/and/ values of type B. Since we are in a strongly typed setting we need
a new type for this, which is essentially an algebraic datatype
definable by (also the internal construction is different, I think)

datatype 'a + 'b = Inl 'a | Inr 'b

here the Inl and Inr are the left and right injections. To extract
values you can just use pattern matching.

fun is_Inl where
is_Inl (Inl _) = True"
| is_Inl (Inr _) = False"

Hope this helps.

cheers

chris

Email Gateway (Aug 18 2022 at 18:14):

From: John Munroe <munddr@gmail.com>
Thanks for the reply. I've just tested

datatype 'a + 'b = Inl 'a | Inr 'b

but it complains about

*** Outer syntax error: name declaration expected,
*** but keyword + was found

It works if I instead have

datatype ('a, 'b) sum = Inl 'a | Inr 'b

Should this produce the same effect?

Using your is_Inl function, how should I then test that if a constant
is of the type A, then is_Inl returns True? is_Inl takes an input of
type 'a + 'b (or ('a,'b) sum, in my case), so how do I supply a
constant of type A?

Thanks

John

Email Gateway (Aug 18 2022 at 18:14):

From: John Munroe <munddr@gmail.com>
OK. I suspect I'm doing something wrong here, but here's what I have:

typedecl A
typedecl B
datatype ('a, 'b) sum = Inl 'a | Inr 'b

fun is_Inl where
is1: "is_Inl (Inl _) = True"
| is2: "is_Inl (Inr _) = False"

axiomatization
inst_parent_type :: "(A,B) sum" and
inst_child_type :: A
where
ax1: "Inl inst_child_type = inst_parent_type"

lemma "is_Inl inst_parent_type"
apply (simp add: is1 ax1)

I'm guessing that the lemma tests whether the type of
'inst_parent_type', i.e. (A,B) sum, has a left injection, i.e. whether
there exists an instance of the "left" child type. Axiom ax1 asserts
that 'inst_child_type' is the left injection. So, should the lemma be
provable?

This approach is supposed to imitate subtyping, but it seems to
require that an instance of the "parent type" to be constructed in
order to do any reasoning about subtypes. If I'm right, then it's
somewhat more restrictive because such an instance must be first
assumed to exist.

Any clarification on this will be much appreciated!

Thanks

John

Email Gateway (Aug 18 2022 at 18:15):

From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 25/08/11 06:08, John Munroe wrote:

OK. I suspect I'm doing something wrong here, but here's what I have:

typedecl A
typedecl B
datatype ('a, 'b) sum = Inl 'a | Inr 'b

fun is_Inl where
is1: "is_Inl (Inl _) = True"
| is2: "is_Inl (Inr _) = False"

axiomatization
inst_parent_type :: "(A,B) sum" and
inst_child_type :: A
where
ax1: "Inl inst_child_type = inst_parent_type"

lemma "is_Inl inst_parent_type"
apply (simp add: is1 ax1)

I'm guessing that the lemma tests whether the type of
'inst_parent_type', i.e. (A,B) sum, has a left injection, i.e. whether
there exists an instance of the "left" child type. Axiom ax1 asserts
that 'inst_child_type' is the left injection. So, should the lemma be
provable?

The lemma asserts that inst_parent_type is of the form "Inl a" for some
a. It is provable "by (simp add: ax1 [symmetric])".

This approach is supposed to imitate subtyping, but it seems to
require that an instance of the "parent type" to be constructed in
order to do any reasoning about subtypes. If I'm right, then it's
somewhat more restrictive because such an instance must be first
assumed to exist.

You don't need to assume anything. Whenever you've got an element a of
type 'a, you've got a corresponding element "Inl a" of type "'a + 'b";
you don't need to assume this.

Given any element c of type "'a + 'b", there is either

• • exactly one element a of type 'a such that "c = Inl a" or
• • exactly one element b of type 'b such that "c = Inr b"
    but not both. is_Inl tells you whether or not it's the first of these
    two possibilities.

Any clarification on this will be much appreciated!

Thanks

John

I hope this has helped.

Tim
<><
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk5VnL4ACgkQ/cBxZIxl6rmpnACfZY9urcaOfhUhfzBxJJ9ip+B3
Kv0AoNc9v9xGgMurYt6dez55S2rFCJIQ
=EjHt
-----END PGP SIGNATURE-----

Email Gateway (Aug 18 2022 at 18:15):

From: John Munroe <munddr@gmail.com>
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.)

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?

Thanks again.

John

Email Gateway (Aug 18 2022 at 18:15):

From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
-----BEGIN PGP SIGNED MESSAGE-----
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?

Tim
<><
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk5VrDcACgkQ/cBxZIxl6rmq5QCcD0zBV6lXqzOkUHQETFj+3Y/4
uPoAoMXhC6dyoX+E9R+E7ehjtcLNr09A
=wgW0
-----END PGP SIGNATURE-----

Last updated: May 01 2024 at 20:18 UTC