Email Gateway (Aug 18 2022 at 17:40): Email Gateway (Aug 18 2022 at 17:40):From: Steve W <s.wong.731@gmail.com>
Hi,
I have a quick question: does anyone know how to define a function taking a
type as an argument? Say, a function f taking the type "nat" as an argument.
Thank you
Steve
Email Gateway (Aug 18 2022 at 17:41):From: Tobias Nipkow <nipkow@in.tum.de>
Types live on the meta-level and are not terms. Hence they cannot be
arguments of functions either. Sorry.
Tobias
Email Gateway (Aug 18 2022 at 17:41):From: Brian Huffman <brianh@cs.pdx.edu>
Well, overloaded constants are a little bit like functions taking
types as arguments. Depending on what you want to do, this kind of
class definition might be useful:
class foo =
fixes f :: "'a itself => int"
instantiation nat :: foo
begin
definition "f (t::nat itself) = 0"
instance ..
end
instantiation list :: (foo) foo
begin
definition "f (t::'a list itself) = 1 + f TYPE('a)"
instance ..
end
Now you can prove things like
lemma "f TYPE(nat list list list) = 3"
by (simp add: f_list_def f_nat_def)
(I haven't tested the above code, so there may be typos.)
Here you can think of "f" as almost a function from types to integers:
You can essentially do primitive recursion over the structure of the
type argument, defining each case with class instantiations.
Email Gateway (Aug 18 2022 at 17:41):From: Lukas Bulwahn <bulwahn@in.tum.de>
If you employ type classes, you could simulate the behaviour of
functions taking types as arguments in a restricted way.
For most applications, the type classes usually suffice.
Lukas
Email Gateway (Aug 18 2022 at 17:41):From: Steve W <s.wong.731@gmail.com>
Thanks. If I change f to a binary function:
class foo =
fixes f :: "int => 'a itself => int"
and with the following instantiation:
instantiation nat :: foo
begin
definition "f 0 (t::nat itself) = 0"
instance ..
end
I get an error on "0::int". It works if 0 is replaced by a free variable
though. Why's that?
Thanks
Steve
Email Gateway (Aug 18 2022 at 17:41):From: René Thiemann <rene.thiemann@uibk.ac.at>
Because "definition" cannot be used with pattern matching on left-hand sides.
Usually, one can use "fun" instead. However, even with "fun" you cannot
do pattern matching on "int" instead of "nat".
However, you might write "f x (t:: nat itself) = (if x = (0 :: int) then 0 else ...)"
René
Email Gateway (Aug 18 2022 at 17:41):From: Brian Huffman <brianh@cs.pdx.edu>
The "definition" command only allows a single equation with variables
for function arguments on the left-hand side. If you want to write
definitions with patterns and/or multiple equations, use "fun",
"function", "primrec", etc.
Email Gateway (Aug 18 2022 at 17:42):From: Steve W <s.wong.731@gmail.com>
Thanks all. One more question: what is the "itself" keyword for in "'a
itself"?
Thanks
Steve
Email Gateway (Aug 18 2022 at 17:42):From: Brian Huffman <brianh@cs.pdx.edu>
2011/5/16 Steve W <s.wong.731@gmail.com>:
Thanks all. One more question: what is the "itself" keyword for in "'a
itself"?
The "itself" is just a type constructor. It is like what you would get
from the following datatype declaration:
datatype 'a itself = Type (* one constructor with no arguments *)
The syntax "TYPE('a)" is an abbreviation for "Type :: 'a itself".
Thanks
Steve2011/5/13 René Thiemann <rene.thiemann@uibk.ac.at>
Thanks. If I change f to a binary function:
class foo =
fixes f :: "int => 'a itself => int"and with the following instantiation:
instantiation nat :: foo
begin
definition "f 0 (t::nat itself) = 0"
instance ..
endI get an error on "0::int". It works if 0 is replaced by a free variable
though. Why's that?Because "definition" cannot be used with pattern matching on left-hand
sides.
Usually, one can use "fun" instead. However, even with "fun" you cannot
do pattern matching on "int" instead of "nat".However, you might write "f x (t:: nat itself) = (if x = (0 :: int) then 0
else ...)"René
--
René Thiemann mailto:rene.thiemann@uibk.ac.at
Computational Logic Group
http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
Email Gateway (Aug 18 2022 at 17:43):From: s.wong.731@gmail.com
I see. But, now I have a slightly different problem:
class foo1 =
fixes f :: "nat => 'a itself => bool"
consts
a :: "nat"
b :: "nat"
instantiation nat :: foo1
begin
definition "fs (t::nat itself) = (if s = a then True else False)"
instance ..
end
lemma "fa TYPE(nat) = True"
by (simp add: f_nat_def)
This is fine. But
lemma "fb TYPE(nat) = False"
by (simp add: f_nat_def)
doesn't seem to prove it. Can the simplifier not interpret the else clause?
Thanks
Steve
Email Gateway (Aug 18 2022 at 17:43):From: Tjark Weber <webertj@in.tum.de>
Steve,
On Tue, 2011-05-17 at 14:46 +0000, s.wong.731@gmail.com wrote:
This is fine. But
lemma "f b TYPE(nat) = False"
^ There should be a space between f and b.
by (simp add: f_nat_def)doesn't seem to prove it. Can the simplifier not interpret the else
clause?
The simplifier doesn't know whether a and b are equal or not. Just
because these two constants have different names, they don't have to be
distinct.
Kind regards,
Tjark
Email Gateway (Aug 18 2022 at 17:43):From: s.wong.731@gmail.com
With the example, would it be possible to let f be a parameter of a locale
instead, ie
locale A1 =
fixes f :: "nat => 'a itself => bool"
defines "fs (t::nat itself) = (if s = a then True else False)"
complains about the operand "t::nat itself". Is it asking for "nat" to be a
parameter?
Thanks
Email Gateway (Aug 18 2022 at 17:43):From: Brian Huffman <brianh@cs.pdx.edu>
The problem is that the types don't match: You've specified in the
"fixes" clause that f should take an argument of type "'a itself", but
in the "defines" clause the argument has type "nat itself". Try the
following:
consts a :: nat
locale A1 =
fixes f :: "nat => 'a itself => bool"
defines "f s (t::'a itself) == (if s = a then True else False)"
Also note that you must use meta-equality (== or \<equiv>) in the
defines clause, rather than ordinary object-equality (=).
Email Gateway (Aug 18 2022 at 17:43):From: s.wong.731@gmail.com
The problem is that the types don't match: You've specified in the
"fixes" clause that f should take an argument of type "'a itself", but
in the "defines" clause the argument has type "nat itself". Try the
following:
consts a :: nat
locale A1 =
fixes f :: "nat => 'a itself => bool"
defines "fs (t::'a itself) == (if s = a then True else False)"
Also note that you must use meta-equality (== or \) in the
defines clause, rather than ordinary object-equality (=).
Sure. But what if f is to be overloaded? Eg,
instantiation nat :: foo
begin
definition d1: "fs (t::nat itself) = (if s = a then True else False)"
instance ..
end
instantiation real :: foo
begin
definition d2: "fs (t::real itself) = (if s = a then False else True)"
instance ..
end
but with 'f' and the definitions inside a locale.
Thanks again
Steve
- Brian
Email Gateway (Aug 18 2022 at 17:44):From: Brian Huffman <brianh@cs.pdx.edu>
I am sorry, but this is not possible. Functions that are fixed by a
"fixes" clause in a locale cannot be overloaded or polymorphic; they
each must have a single, fixed type. (They may mention type variables
like 'a, but this does not make them polymorphic -- such type
variables are treated as fixed types within the locale context).
A workaround may be possible, though: You can define "f" at the top
level, making it polymorphic or overloaded. Then you can put
assumptions about the definitions of "f" at various types inside a
locale. For example:
class foo =
fixes f :: "nat => 'a itself => bool"
consts a :: nat
locale A =
assumes "f s TYPE('a::foo) = (if s = a then True else False)"
assumes "f s TYPE('b::foo) = (if s = a then False else True)"
Later on, you could interpret locale A with type 'a instantiated as
nat, and type 'b as real.
Email Gateway (Aug 18 2022 at 17:44):From: s.wong.731@gmail.com
On May 20, 2011 2:52pm, Brian Huffman <brianh@cs.pdx.edu> wrote:
2011/5/20 s.wong.731@gmail.com>:
The problem is that the types don't match: You've specified in the
"fixes" clause that f should take an argument of type "'a itself", but
in the "defines" clause the argument has type "nat itself". Try the
following:
>
consts a :: nat
>
locale A1 =
fixes f :: "nat => 'a itself => bool"
defines "fs (t::'a itself) == (if s = a then True else False)"
>
Also note that you must use meta-equality (== or \) in the
defines clause, rather than ordinary object-equality (=).
>
Sure. But what if f is to be overloaded? Eg,
>
instantiation nat :: foo
begin
definition d1: "fs (t::nat itself) = (if s = a then True else False)"
instance ..
end
>
instantiation real :: foo
begin
definition d2: "fs (t::real itself) = (if s = a then False else True)"
instance ..
end
>
but with 'f' and the definitions inside a locale.
I am sorry, but this is not possible. Functions that are fixed by a
"fixes" clause in a locale cannot be overloaded or polymorphic; they
each must have a single, fixed type. (They may mention type variables
like 'a, but this does not make them polymorphic -- such type
variables are treated as fixed types within the locale context).
A workaround may be possible, though: You can define "f" at the top
level, making it polymorphic or overloaded. Then you can put
assumptions about the definitions of "f" at various types inside a
locale. For example:
class foo =
fixes f :: "nat => 'a itself => bool"
consts a :: nat
locale A =
assumes "fs TYPE('a::foo) = (if s = a then True else False)"
assumes "fs TYPE('b::foo) = (if s = a then False else True)"
Later on, you could interpret locale A with type 'a instantiated as
nat, and type 'b as real.
I see. Do you know why only fixed types are supported inside locales? Is it
a restriction imposed by the logic?
Steve
- Brian
Last updated: Apr 20 2024 at 04:19 UTC