## 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: Sep 25 2022 at 23:25 UTC