Manuel Eberl (May 29 2020 at 10:30): Manuel Eberl (May 29 2020 at 10:30):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:
adhoc_overloading? I don't actually understand how it works. Perhaps we should ask the people who implemented that.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! Lukas Stevens (May 29 2020 at 10:37):Out of interest: has the idea of adding type constructors ever been discussed on the mailing list?
Manuel Eberl (May 29 2020 at 11:01):What do you mean, "adding type constructors"? We have type constructors.
Lukas Stevens (May 29 2020 at 11:04):Sorry I meant type constructors for type classes which would enable monads etc.
Manuel Eberl (May 29 2020 at 11:05):I don't think that has ever been discussed. It would probably require a massive overhaul of Isabelle's type class system.
Mathias Fleury (May 29 2020 at 11:10):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.
Mathias Fleury (May 29 2020 at 11:15):»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?
Manuel Eberl (May 29 2020 at 11:21):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.
Manuel Eberl (May 29 2020 at 11:22):I also don't understand your other comment about the sort constraints.
Mathias Fleury (May 29 2020 at 11:23):The order of the imports matters in some cases (like multiple constants with the same name).
Manuel Eberl (May 29 2020 at 11:25):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)
Mathias Fleury (May 29 2020 at 11:36):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?
Manuel Eberl (May 29 2020 at 12:17):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.
Manuel Eberl (May 29 2020 at 14:53):I meant "checking phase".
Manuel Eberl (Jun 19 2020 at 11:44):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: Dec 21 2024 at 12:33 UTC