CakeML / CakeML/pure

Semantics for TypeClassLang

Open
#62 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Standard ML
Stars
44
Forks
5
PR merge metrics
No merged PRs in 30d

Description

**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:
```haskell
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.

```haskell
exists :: Eq a => a -> [a] -> Bool
exists x [] = False
exists x (y:ys) = if x == y then True else exists x ys
```
`--becomes-->`
```haskell
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]]`

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.