Typechecking a Surface Language Considered Harmful!

Let me start by sharing two lines of code:

tjExp :: Judgement Exp Rho C
tjExp (App fun arg) expTy ve = do
(funTy, qfun) <- inferBy tjExp fun ve
(argTy, resTy) <- unifyFun funTy
(_ , qarg) <- typecheckBy tjExpPoly arg argTy ve
(r , q) <- matchSigmaRho resTy expTy --inst RULE
return (r, qfun ++ toC qarg ++ toC q)

It is a typing judgement for expression (Exp) that expects the type, both in inference and typechecking, to be of Rho type. It also generates constraints of type C (normal constraints plus implications).
At first, it uses typing judgement for expressions (tjExp) to infer a type for the function, unifies the inferred type with a type of the form sigma1 -> sigma 2. Later, the argument (arg) is checked to have the expected polymorphic type (notice tjExpPoly) . After all these, the type of the result of the application (resTy) should be checked to match the expected type (expTy). Since the judgement is bidirectional, i.e. works for both type inference and typechecking, expTy is simply of type Maybe Rho. Therefore in type inference, matchSigmaRho simply needs to instantiate the polymorphic type.

Now let us consider typechecking expressions with a negation operator:

tjExp :: Judgement Exp Rho C
tjExp (NegApp eexp) s ve = ???

How do you write a “clean” code for this case?
In the beginning of the project, I was trying hard to typecheck each expression as-is, meaning, I didn’t want to transform them into a simpler form. I ended up having loads of duplicated code full of bugs! Here is my current implementation:

tjExp :: Judgement Exp Rho C
tjExp e@(NegApp eexp) s ve =
tjExp (desugar "" e) s ve
desugar :: String -> Exp -> Exp
desugar _ (NegApp eexp) =
(App (Var (UnQual (Ident "negate"))) eexp)

Now, let me list cons & pros list of typechecking a surface, in contrast to a core, language:

  • The semantic of a language is mostly defined for the core representations. Having a system based on the surface representation includes lots of bogus assumptions (corner cases!).
  • Common sense of the programmers disagrees on the surface and unifies on the core.
  • In general, it is much harder to write code for the surface language, due to it’s richness, and it increases chances of writing defects.
  • Scientific literature, mostly when it comes to typechecking, discusses the core representations. Here, I follow Mark Jones’s view (Typing Haskell in Haskell); I believe if new features and extensions are introduced to the system, since ‘The whole is greater than sum of its parts’, it is necessary to revisit the design as a whole. If sum of all the transformations, from surface to core, is sound, clear and clean; the surface language can safely be ignored.
  • When new features are introduced to the language, having one system focusing on the surface and one on the core (latter is the natural choice) potentially leads to inconsistencies.
  • Pros:

  • Error messages! Here my belief is a little controversial; I believe reversibility in practice can be orthogonal to the development itself! the transformations from the surface presentation to the core is almost
    one-to-many. That is because, mostly, the core language AST is subset of the surface AST. This means, with a correct design there would be no information lost in the transformation. A currently existing bidirectionlization system
    can automatically map the converted expressions back to the original.[1]
  • Typechecking takes longer to terminate. Well, it happens at compile time right?
  • Having all these in my head, I am thinking of yet another H?E project… something like Haskell-Transformation-Exts or Haskell-Desugaring-Exts. That would be beneficial to people who want to work on Haskell’s AST.

    [1] We ( Meng Wang, Emil Axelson and me) already implemented the idea in a Haskell EDSL (Feldspar) which is converted to C code.

    About Shayan

    Researcher/Programmer at Chalmers University of Technology
    This entry was posted in Articles. Bookmark the permalink.

    Leave a Reply

    Fill in your details below or click an icon to log in:

    WordPress.com Logo

    You are commenting using your WordPress.com account. Log Out / Change )

    Twitter picture

    You are commenting using your Twitter account. Log Out / Change )

    Facebook photo

    You are commenting using your Facebook account. Log Out / Change )

    Google+ photo

    You are commenting using your Google+ account. Log Out / Change )

    Connecting to %s