Stream: Beginner Questions

Topic: Sum of functions

Nicolò Cavalleri (Jun 10 2021 at 18:13):

Where is the exact point in the HOL library where it is proven that if the type `'a` has an instance as a real_vector then functions valued in `'a` also do? How do I find out these kind of things? On Lean ctrl+click on + takes you to the instance where that type has been given addition but in Isabelle it takes you to the point where + is introduced in Isabelle

Manuel Eberl (Jun 10 2021 at 19:45):

There is no `real_vector` instance for functions in either `HOL` or `HOL-Analysis`. What library are you using exactly?

Manuel Eberl (Jun 10 2021 at 19:48):

There is one in `Lp.Functional_Spaces` in the AFP…

Manuel Eberl (Jun 10 2021 at 19:49):

I don't know if there is a general way to find out where exactly a particular typeclass instance for a particular type constructor was proven.

Nicolò Cavalleri (Jun 10 2021 at 22:50):

I am using the smooth manifolds library. I guess

``````instance "fun" :: (type, real_vector) real_vector
by standard (auto simp: scaleR_fun_def algebra_simps)
``````

is then the point where such instance is defined... What is exactly the syntax ` "fun" :: (type, real_vector)`?

Jakub Kądziołka (Jun 10 2021 at 22:55):

`instance a :: (b, c) d` means that `'t 'u a :: d` if `'t :: b` and `'u :: c`

Manuel Eberl (Jun 11 2021 at 08:52):

And "fun" is the internal name of the function type constructor. When you write `'a ⇒ 'b`, the internal representation of that type is `('a, 'b) fun`.

Manuel Eberl (Jun 11 2021 at 08:53):

I see, the Smooth Manifold entry defines its own vector space instance for functions – presumably in the same way as the `Lp` entry.

Nicolò Cavalleri (Jun 11 2021 at 10:51):

Can I write the instantiation in an equivalent way as

``````instantiation "'a ⇒ ('b :: real_vector)" :: real_vector
``````

somehow? It tells me `Undefined type name: "'a ⇒ ('b :: real_vector)"`

Manuel Eberl (Jun 11 2021 at 10:53):

No, you have to write `instantiation "fun" :: (type, real_vector) real_vector`. The bit before the `::` has to be a type constructor.

Nicolò Cavalleri (Jun 11 2021 at 10:57):

Ok, my final goal is to put an instance of `real_vector` on the type `('a × (('a ⇒ real) ⇒ real))` which ignores the first coordinate and treats pairs as if they were they second coordinate. Does this mean that I have to put an instance on a generic product of a type and a real vector space? This will probably collide with the instance of product of vector spaces which is more standard I guess

Nicolò Cavalleri (Jun 11 2021 at 10:58):

Indeed it says

``````Conflict of type arities:
prod :: (type, real_vector) cancel_ab_semigroup_add and
``````

Manuel Eberl (Jun 11 2021 at 10:58):

You cannot do that in Isabelle. Typeclass instances must always be for a type constructor.

Manuel Eberl (Jun 11 2021 at 10:59):

What you are trying to do would require something like `FlexibleInstances` and `OverlappingInstances` in Haskell, which the Isabelle type class system just doesn't support.

Manuel Eberl (Jun 11 2021 at 10:59):

The only way around this would be to introduce a type clone of `'a × (('a ⇒ real) ⇒ real)` with `type_definition`, then you can instantiate it in whichever way you want

Nicolò Cavalleri (Jun 11 2021 at 11:00):

Manuel Eberl said:

The only way around this would be to introduce a type clone of `'a × (('a ⇒ real) ⇒ real)` with `type_definition`, then you can instantiate it in whichever way you want

Ok thanks this is what I was looking for!

Manuel Eberl (Jun 11 2021 at 11:00):

Sorry, type classes in Isabelle are just not very flexible… It's a known problem.

Lukas Stevens (Jun 11 2021 at 11:06):

It would be nice to have some kind of deriving via typedef mechanism like in Haskell. This wouldn't require any changes to the core typeclass mechanism.

Lukas Stevens (Jun 11 2021 at 13:31):

Lukas Stevens said:

It would be nice to have some kind of deriving via typedef mechanism like in Haskell. This wouldn't require any changes to the core typeclass mechanism.

A topic for a student perhaps?

Last updated: Aug 13 2022 at 06:26 UTC