Define a semantics for annotated TypeClassLang via translation to PureLang
This should be a clean, declarative specification of dictionary construction which is naive enough to be "obviously right" on inspection - this is effectively the reference semantics for TypeClassLang. It should use the annotations present in TypeClassLang to construct dictionaries for each instance at their use-sites. Various examples of dictionary constructions can be found in literature and online, but in a recent meeting we discussed the example below.
Note that PureLang does not have dictionaries so we will use tuples instead. This will allow existing reasoning and optimisations in PureLang to target type class dictionaries with minimal changes.
Consider the following Haskell code:
class Eq a where
(==) :: a -> a -> Bool
class Eq a => Ord a where
(<) :: a -> a -> Bool
instance Eq Int where
(==) x y = intEq x y -- where intEq :: Int -> Int -> Bool
instance Eq a => Eq [a] where
(==) l1 l2 = (null l1 && null l2) || head l1 == head l2 && tail l1 == tail l2
Each class declaration effectively declares a dictionary type:
Eq a --becomes--> eqDict a := { (==) :: a -> a -> Bool }
Ord a --becomes--> ordDict a := { eq :: eqDict a ; (<) :: a -> a -> Bool }
Each instance declaration specifies how to construct a dictionary of the relevant type.
In particular, in general instance produce functions which accept dictionaries corresponding to the context and produce the desired instance dictionary.
Eq Int --becomes--> (eqInt :: eqDict Int) := { (==) = \ x y -> intEq x y }
Eq a => Eq [a] --becomes--> (eqList :: eqDict a -> eqDict [a]) :=
\ eqA -> { (==) = \ l1 l2 -> ... || eqA.(==) (head l1) (head l2) && ... }
Above we can see the use of eqA.(==) to select an equality operator.
Overloading resolution decides which dictionary is needed at any given point and how to construct it.
Below, we can see how we expect exists to translate: it takes an extra parameter corresponding to the context Eq a, and indexes into this dictionary to select the equality operator.
exists :: Eq a => a -> [a] -> Bool
exists x [] = False
exists x (y:ys) = if x == y then True else exists x ys
--becomes-->
exists' :: eqDict a -> a -> [a] -> Bool
exists' eqA x [] = False
exists' eqA x (y:ys) = if eqA.(==) x y then True else exists' eqDictA x ys
A concrete application of exists [1] [[1,2],[3] must construct the dictionary corresponding to the Eq [Int] instance.
Overloading resolution will show us that we must construct exists' (eqList eqInt) [1] [[1,2],[3]]
Define a semantics for annotated TypeClassLang via translation to PureLang
This should be a clean, declarative specification of dictionary construction which is naive enough to be "obviously right" on inspection - this is effectively the reference semantics for TypeClassLang. It should use the annotations present in TypeClassLang to construct dictionaries for each instance at their use-sites. Various examples of dictionary constructions can be found in literature and online, but in a recent meeting we discussed the example below.
Note that PureLang does not have dictionaries so we will use tuples instead. This will allow existing reasoning and optimisations in PureLang to target type class dictionaries with minimal changes.
Consider the following Haskell code:
Each class declaration effectively declares a dictionary type:
Each instance declaration specifies how to construct a dictionary of the relevant type. In particular, in general instance produce functions which accept dictionaries corresponding to the context and produce the desired instance dictionary.
Above we can see the use of
eqA.(==)to select an equality operator.Overloading resolution decides which dictionary is needed at any given point and how to construct it. Below, we can see how we expect
existsto translate: it takes an extra parameter corresponding to the contextEq a, and indexes into this dictionary to select the equality operator.--becomes-->A concrete application of
exists [1] [[1,2],[3]must construct the dictionary corresponding to theEq [Int]instance. Overloading resolution will show us that we must constructexists' (eqList eqInt) [1] [[1,2],[3]]