RSS

Monthly Archives: January 2012

Decoupling type classes

(I posted this idea to Haskell Cafe some days ago and got interesting respons from Dominique Devriese, who implemented instance arguments [1,2] (Agda’s equivalence of type classes). The disucssion has been really interesting, so I decided to collect and organize the ideas into a coherent post here. Some syntax is borrowed from their work.)

This post relates the three ideas together: type classes, implicit parameters, and typed dynamic scoping. The first two are researched into some degree but their relationship and design are still subject to debates. The latter is my own analogy which appears to be really helpful clarifying those design decisions.

For the impatient, I have bulletted points with all the main ideas in this post here:

  • We can achieve the same or more expressiveness of type classes without using dictionaries. We just need implicit parameters.
  • Implicit parameters and their types can be fully inferred.
  • Implicit parameters can express MPTCs.
  • Type classes can be thought of as dynamic typing, though more disciplined.

To group, or not to group

Haskell’s type classes tie the two concepts “overloading” and “grouping” together, but in fact they are not necessarily related. Decoupling those two concepts has several benefits:

  • It makes the type system more flexible.
  • It makes the implementation more modular.
  • It frees us from the need to pass a whole dictionary when we only use one function in it.

I’m curious why we need to group those functions into a type class, instead of using them directly as overloaded functions. So I built an experimental type system which “decouples” the dictionary. Instead of passing a dictionary, it passes individual “implicit parameters” to the function. Each implicit parameter corresponds to an “undefined variable” in the function. Those implicit parameters are type inferenced and can contain type parameters just as the functions in a type class. Similarly, they are resolved by their types in the call site’s scope.

The convenience of this approach compared to Haskell’s type classes is that we no longer require a user of a type class to define all the methods in a type class. For example, a user could just define a method + without defining other methods in the Num class: -, *, … He can use the method + independently. For example, if + is defined on the String type to be concatenation, we can use + in another function:

weirdConcat x y = x + y + y

This has a utility, because the methods in the Num class don’t “make sense” for Strings except +, but the current type class design requires us to define them. This is burdensome. By separating the Num class into individual overloaed functions, we enables this kind of overloading without any extra work.

Then a question arises: how do we relate the types of functions if we no longer have this grouping? For example, for the Monad class, we expect return to be of type (a -> m a) if (>>=) is of type (m a -> (a -> m b) -> m b).

The answer is to use a polymorphic record to group the functions when needed, then reference the functions through the record.

Thus we have delegated the task of overloading to separate overloaded functions, and the task of grouping to records. This is a more modular design compared to the original type class system of Haskell.

Expressing MPTC

There is another benefit of this decoupling: it is expressive enough to subsume MPTC. Here is why: because the methods are no longer grouped, there is no longer a “common” type parameter to the methods. Thus we can easily have more than one parameter in the individual methods and conveniently use them as MPTC methods.

For example,

overload g
 ... ...
f x (Int y) = g x y

Notice that in my system, there are no explicit declarations containing type variables. The declaration “overload g” is all that is needed. The system infers f’s type as:

a -> Int -> {{g: a -> Int -> b}} -> b

Here it automatically infers the type for g (a -> Int -> b) just from its usage inside f, as if we have written a type class definition like:

class G a where
 g :: a -> Int -> b

So in this system, not only we don’t need to defined type classes, we don’t even need to declare the types of the overloaded functions! We can infer them from their usage and different calls to the same function don’t even need to have the same type! All it takes is:

overload g

And even this is not really necessary. It is for sanity purposes – to avoid inadvertent overloading of unbound variables.

So if g is used as:

f x y (Int z) = g x z y

then we infer its type as:

a -> b -> Int -> {{ g :: a -> Int -> b -> c}} -> c

and g will be equivalent to the one you would have defined in a MPTC method.

Some implementation details

Here is how it can be implemented. When we see an “undefined” variable in a function definition which has been declared as “overloaded function”, we store the function name, and the type variables that are associated with it. For example,

overload g -- (explicitly declare g as an overloaded function)

f x y (String s) = ...
...
let z = g x s y in
...
...

We don’t know what x and y are, but we know from the body of f that their types satisfy this pattern: g a String b. Thus we store this pattern constraint as an extra (implicit) argument in the type of f:

f :: a -> b -> String {{g: g a String b}}

We may have multiple such arguments.

At the call sites of f, we look for a function g in the scope that satisfies the pattern g a String b, but we don’t pass on the substitution, so they remain polymorphic. Once found, the function is passed as an extra parameter to f. This is essentially dictionary passing, but without grouping. It can be also more efficient because the parameters may be stored in registers.

Here g is explicitly declared as “overloaded”, although my experimental system doesn’t need this. Any undefined variable inside function body automatically becomes overloaded. This may cause unintended overloading and it catches bugs late. That’s why we need the “overload” declarations.

But the automatic overloading of the undefined may be useful in certain situations. For example, if we are going to use Haskell as a shell language. Every “command” must be evaluated when we type them. If we have mutually recursive definitions, the shell will report “undefined variables” either way we order the functions. The automatic overloading may solve this problem. The undefined variables will temporarily exist as automatic overloaded functions. Once we actually define a function with the same name AND satisfies the type constraints, they become implicit parameters to the function we defined before. If we call a function whose implicit parameters are not associated, the shell reports error very similar to Haskell’s “type a is not of class Num …”

Type classes as typed dynamic scoping

It appears to be helpful to think of the calls to overloaded functions as referencing dynamically scoped variables. They are dispatched depending on the bindings we have in the call site’s scope (and not the scope where the method is defined!). So it is very much similar to the much-hated dynamic scoping. But the dispatching is more disciplined — it doesn’t just match the name. It must match both the name and the inferred type. So in general it is useful and doesn’t cause trouble.

This intuition also explains why local instances shouldn’t be allowed, because if we capture the variables at the definition site, the method call becomes “statically scoped”.

Let me post an example from Oleg:

foo x =
 let overload bar (x:Int) = x + 1
 in \() -> bar x

baz =
 let overload bar (x:int) = x + 2
 in foo (1::Int)

Here at the call site foo (1::Int), bar should be resolved to the one inside baz, and not the one inside foo. My analogy to “dynamic scoping” is useful to understand the reason here. If we capture the bar inside foo’s definition site, it would correspond to “lexical scoping”.

Footnotes:

[1] https://lirias.kuleuven.be/handle/123456789/304985
[2] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments

 
Leave a comment

Posted by on January 16, 2012 in programming languages, types

 

ydiff: a structural program comparison tool

(Click on the above picture to see it in action. See the end of the post for more demos)

Motivation

I have been imagining a world where programs are not represented as text, but as data structures. They will be edited not with text editors, but with structural editors, which create and manipulate the abstract syntax trees (AST) directly. In such a programming environment, the line-by-line diff utilities and version control tools will stop working, because there are no longer “lines” or “words” in programs.

ydiff is a proof-of-concept for handling this situation. It is a diff tool designed for “structural programming”.

Currently ydiff takes pains to parse program text into ASTs, but hopefully in the future programs will be stored directly as data structures so that the parsing step can be skipped. This will enable this kind of tool to extend to all programming languages effortlessly.

Features

  • Language-aware. ydiff parses programs, understands basic language constructs and will not make non-sensical comparisons. For example it will not compare a string “10000” with an integer 10000 even though they look very similar. Also, it tries to match functions with the same name before it attempts to destruct and compare functions of different names.
  • Format insensitive. The comparison result will not be affected by different number of white spaces, line breaks or indentation. For example, ydiff will not produce a large diff just because you surrounded a block of code with if (condition) {…}.
  • Moved code detection. ydiff can find refactored code — renamed, moved, reordered, wrapped, lifted, combined or fragmented code. Refactored code can be detected however deep they are into the structures.
  • Human-friendly output. The output of ydiff is designed for human understanding. The interactive UI helps the user navigate and understand changes efficiently.

These properties make ydiff helpful for understanding changes. It may also be possibly used for detecting plagiarism in programming classes or copyright infringement of code. For large-scale use cases you may be more interested in MOSS, but ydiff is fundamentally more accurate because it parses programs.

Demos

Here are some interactive HTML demos with a pretty nice UI design. The left and right windows are always locked in their relative position. A mouse click on changed, moved or unchanged nodes will highlight the matched nodes and scroll the other window to match. After that, the windows will be locked into their new relative position for browsing.

Okay, here are the demos.

  • Scheme Demo1. ydiff’s algorithm diffing itself (between the first version on GitHub and the latest version).
  • Scheme Demo 2. Comparison of the original miniKanren from Professor Dan Friendman and the version I modified in order to support condc, a “negation operator”. Pay attention to the function unify, whose major part is moved into unify-good.
  • Emacs Lisp. Comparison of two versions (v20 and v23) of Taylor Campbell’s paredit-mode, a structural editing mode of emacs for Lisp programs.
  • Clojure. Compare the first commit of Typed Clojure with its recent version.
  • Arbitrary S-expressions. Trying to find a bug in an optimizing pass of my Scheme compiler by comparing the IRs (represented as S-expressions).
  • Python. ydiff has a completely separate implementation in Python (named “PyDiff”), which can diff two Python programs. This is a comparison of two implementations of a small list library that I wrote, which implements Lisp-style lists. The first implementation uses recursive procedures while the second uses Python’s generator syntax and is iterative. Pay some attention to append, whose code is moved inside another function appendAll.
  • Javascript. Comparison between two major revisions of the UI code of ydiff itself.
  • C++ demo1 and C++ demo2. There are two demos for C++. The first demo compares two versions of the d8 Javascript debugger from the V8 project(v3404 from 2009 and v8424 from 2011). The second demo compares V8’s simulators for two different processors (MIPS and ARM).The d8 demo is especially interesting because by clicking on the lines of the method Shell::Initializein the old version, it can be clearly observed that its body has been distributed into several procedures in the new version:
    Shell::Initialize
    Shell::CreateGlobalTemplate
    Shell::RenewEvaluationContext
    Shell::InstallUtilityScript

    Also the major part of Shell::Main is moved into the helper Shell::RunMain.

Get the code

ydiff is an open source project. You can follow its development on github: yinwang0/ydiff or get its source code from there.

 
Comments Off on ydiff: a structural program comparison tool

Posted by on January 3, 2012 in algorithms, programming languages, tools