There is a well-known problem with Isabelle's constant overloading: Suppose we want to define an `nth`

function with the type

```
nth :: 'a foo ⇒ 'b ⇒ 'a
```

and concrete instances such as:

```
nth :: 'a poly ⇒ nat ⇒ 'a (polynomials)
nth :: 'a fps ⇒ nat ⇒ 'a (formal power series)
nth :: 'a fps ⇒ int ⇒ 'a (formal Laurent series)
nth :: ('a, 'n) ⇒ 'n ⇒ 'a (vectors)
```

One would want to have something like this to have common notation for these operations (e.g. infix `$`

).

The problem is now that Isabelle's overloading does not support type constructors. One would have to declare the constant as

```
nth :: 'a ⇒ 'b ⇒ 'c
```

but now there is no link at all between the different type variables. Even if we know that `p`

is a polynomial, writing `nth p n`

will give `nth`

the type `'a poly ⇒ 'b ⇒ 'c`

so that we have to manually annotate everything.

In my opinion, the cleanest solution to this would be to allow specifying functional dependencies for overloaded constants (similarly to what is done for multi-parameter type classes in Haskell).

For the above, one could specify that the type of the first argument of `nth`

uniquely determines the other two. This could be implemented by a checking phase that attempts to match the types of each available overloading instance and, if there is a unique one, applies the dependencies by adding type constraints.

This should also work for things like the monadic bind and return operators.

Open questions:

- Does this work?
- Should there be a type error if the instance is
*not*unique or if none exists? Probably yes. - How does this differ from
`adhoc_overloading`

? I don't actually understand how it works. Perhaps we should ask the people who implemented that. - Perhaps one should make it so that for the determination of the fitting instance, type parameters that are determined by others are left as variables before unification. That way, something like
`nth (p :: 'a poly) (-1::int)`

will result in a type error`nat ≠ int`

instead of the less informative ‘no instance found’. That would be a major advantage over`adhoc_overloading`

!

Out of interest: has the idea of adding type constructors ever been discussed on the mailing list?

What do you mean, "adding type constructors"? We have type constructors.

Sorry I meant type constructors for type classes which would enable monads etc.

I don't think that has ever been discussed. It would probably require a massive overhaul of Isabelle's type class system.

My intuition says that your approach will run into problems if nth requires sort constraints that do not appear in the rest of the formula. But I am not sure.

»Should there be a type error if the instance is not unique or if none exists? Probably yes.«

Isn't the Isabelle way is to take the first one such that the order of the imports matters?

Not sure what you mean by that. You cannot have overlapping constant specifications (that would be logically inconsistent). Underspecified constants are okay. If you mean type classes: each type either has zero or one instantiations of a type class. If you have two theories that each have an instantiation for that type, the theory merge will just fail.

I also don't understand your other comment about the sort constraints.

The order of the imports matters in some cases (like multiple constants with the same name).

For illustration, here is a working ‘mock up’ in Haskell of how I think it should work in Isabelle as well. Note that the error messages work out exactly how I would like them to work out in Isabelle as well.

```
{-# LANGUAGE FunctionalDependencies, FlexibleInstances #-}
class Nth a b c | a -> c, a -> b where
nth :: a -> b -> c
data Nat = Nat Int
data MyType = MyType
data MyOtherType = MyOtherType
data Poly a = Poly (Nat -> a)
data FPS a = FPS (Nat -> a)
data FLS a = FLS (Int -> a)
data Vec a n = Vec (n -> a)
instance Nth (Poly a) Nat a where nth = undefined
instance Nth (FPS a) Nat a where nth = undefined
instance Nth (FLS a) Int a where nth = undefined
instance Nth (Vec a n) n a where nth = undefined
myPoly = undefined :: Poly MyType
myFPS = undefined :: FPS MyType
myFLS = undefined :: FLS MyType
myNat = Nat 0
myInt = 0 :: Int
myVec = undefined :: Vec MyType MyOtherType
test1 = nth myPoly myNat
test2 = nth myFPS myNat
test3 = nth myFLS myInt
-- not enough information to determine instance
test4 = nth undefined myNat -- ERROR: Non type-variable argument in the constraint: Nth a Nat c
-- inferred type for dependent argument contradicts actual type
test5 = nth myFLS myNat -- ERROR: Couldn't match type ‘Int’ with ‘Nat’
:t nth myFPS -- nth myFPS :: Nat -> MyType
:t nth myFLS -- nth myFLS :: Int -> MyType
:t nth myVec -- nth myVec :: MyOtherType -> MyType
```

@ ‘The order of the imports matters in some cases (like multiple constants with the same name).’

Yes, for the translation of short name into last name the import order does matter. But this is definitely something we would want to avoid here. Especially because in our case, the instances cannot overlap by design (this is forbidden by the logic), so if we have more than one possible instance, that just means the type is not specific enough.

This *must* be fixed by the user by adding additional type constraints. Otherwise the user cannot even use the constant at all since they will not be able to unfold the definition.

(Of course, there may be rare instances where, for technical reasons, you do want to write down this generic constant. But one could allow disabling the error for these cases)

Do you have any idea if it is sufficient to add a parsing pass https://isabelle.in.tum.de/dist/library/Doc/Implementation/Syntax.html?

Pretty sure this is checking, not parsing. We can just add a checking translation (similarly to what `adhoc_overloading`

does). Perhaps another one for the error messages at the very end of checking.

I meant "checking phase".

Update: I talked this over with Florian. I think functional dependencies don't work that great for Isabelle, but one could instead give a list of subsets of type variables that each determine the instance uniquely by themselves. For instance, for the monadic bind, which is conceptually `bind :: 'a m ⇒ ('a ⇒ 'b m) ⇒ 'b m`

and would have to have the overloaded type `'a ⇒ ('b ⇒ 'c ⇒ 'c)`

, one could give `{'a}`

and `{'c}`

as determining sets, since each of these allows you to read off the `m`

.

The procedure could be registered as a phase 0 checking phase, which means that it would run intertwined with regular type inference. I'll make a proof of concept implementation as soon as I can figure out how to cleanly and robustly refine types in a checking phase…

Last updated: Nov 11 2024 at 01:24 UTC