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

where

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:

**Cons:**

**Pros:**

*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]

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.