Understanding modify function from THIH (Typing Haskell In Haskell)

Viewed 98

I am reading typing haskell in haskell

Have a hard time understanding this line of coding on p 13

modify ce i c = ce{classes=\j→if I==j then Just c else classes ce j}

Where is j coming from? There is a brief covering on modify but no mentioning of j at all on p 13. On p14, there is a call made to the return (modify ce i (is, [])) under the addClass. This is where I could not figure out. How can a call to modify ce i ( is, [])) be made if there is no j provided? Thanks for any help.

3 Answers

j is still part of the lambda expression

\j -> if i==j then Just c else classes ce j

that defines the value of the classes field. This function is a closure over the values i, c, and ce that modify itself receives as arguments.

It's a like a recursive function: the result of modify ce i c is an value where (for some values ce, i, c, and x)

classes (modify ce i c i) == Just c

and

classes (modify ce i c x) == classes ce x`.

Except instead of classes actually calling itself, modify creates an new value of type ClassEnv that wraps a "smaller" value of the same type. The classes function unwraps that environment one layer at a time until it either finds a matching value for the original argument, or it reaches the initialEnv value for which classes initalEnv _ == Nothing.

j is a lambda parameter. You can give a parameter any name you like. What does it represent? The type signature of modify tells us the first parameter is of type ClassEnv, so you can go read its definition (page 12) to see what type its classes field has.

To add to the other answers, what the author of that paper does is define a very simple map or dictionary using only functions. Normally you might write Map Id Class where Map is from the containers package, but you can also use the type Id -> Maybe Class which then basically is the lookup function for your map type. Then some simple functions can be implemented like this:

type Map k v = k -> Maybe v

singleton :: Eq k => k -> v -> Map k v
singleton k v = \k' -> if k == k' then Just v else Nothing

insert :: Eq k => k -> v -> Map k v -> Map k v
insert k v lookup = \k' -> if k' == k then Just v else lookup k'

union :: Map k v -> Map k v -> Map k v
union lookup1 lookup2 = \k -> case lookup1 k of
  Nothing -> lookup2 k
  v -> v

delete :: Eq k => k -> Map k v -> Map k v
delete k lookup = \k' -> if k == k' then Nothing else lookup k'

lookup :: Map k v -> k -> Maybe v
lookup = id

So, instead of defining the map as a collection of values, you define the map as the lookup function.

An advantage of this approach is that it is simple because it doesn't rely on external dependencies. But it is not so flexible: you cannot, for example, list all the keys and values in the map; and it is slow: lookups need to do a linear number of equality tests.

Related