Faridah Liduan

The motivation of this project to preserve understandable and appropriate error messages of Helium compiler in higher rank types

I took the following approaches as a starting point of this project:

• Extend the language to support rank-2 type
• Rank-2 type can only be specified in the type signatures

Literature

In order to understand and get familiar with the subject, I have to read the following papers:

• Bastiaan Heeren, Juriaan Hage, and S. Doaitse Swierstra, Constraint Based Type Inferencing in Helium, The CP-03 Workshop on Immediate Applications of Constraint Programming, Cork, Ireland, September 29, 2003
• Bastiaan Heeren and Juriaan Hage, Parametric Type Inferencing for Helium, Technical Report
• Simon Peyton Jones and Mark Shields, Practical type inference for arbitrary-rank types, 2003

Reviews

Brief description of the papers that I have read:

• Constraint Based Type Inferencing in Helium- This paper explains how constraint based type inferencing process in Helium in structural ways; starting with a preliminary explanation on types, substitution, and constraints. Then it gives lists of type inference rules used. Finally it describes how the type inference process (generation, ordering, and solving the constraints) is done. It is recommended to read this paper before looking at the implementation.

Type Inference over Higher Rank Type

Current State

• For un-annotated program:
  • if a variable bound by let, where, or top level bindings : a rank-1 type is inferred
  • variables bound by lambda, case, do-notation, list comprehension, or left hand side pattern of a function definition get monotypes (rank-0 types)

• A variable may get a higher-rank type if they can easily be inferred from the context of variable's binding, e.g.

         f :: (forall a. a -> a) -> (Bool, String)
         f g = (g True, g "hello")

     

Here, the type of the argument

 g 

 f 

Some restrictions

• We should give explicit type signature to the higher rank function

• We should supply enough argument to the higher rank function until the position of the polymorphic arguments while defining and calling the function, e.g.

        f1 :: (forall a. a -> a) -> Int -> Char            -- requires at least 1 argument
      
        f2 :: Int -> (forall a. a -> a) -> Bool -> Int     -- requires at least 2 arguments

     

Implementation Steps

While working on this project, I work through the following steps:

• Parsing
  • Modify the parser in order to be able to parse quantified type

• Extend the Type Language
  • Create a new data type to represent rank-2 types, as follows:

         
           data Rank2 = Rank1 TpScheme
                       |Arrow TpScheme Rank2
                       |Rank2_Forall [Int] Rank2   
           

  • Create conversions from existing type representation to rank-2 representation

• Constraint Generation
  • Change constraints generation process for some language constructs
  • Incorporate the rank-2 type information to the generated constraint information

• Solver
  • Add rank-2 heuristics to the type graph solver
    • How?
      • Get the collected rank-2 constraint information
      • Get the source of errors
      • Perform some checks
      • Use results of checking and rank-2 constraint information to produce new error messages
    • Remarks
      • Existing heuristics are still preserved
      • Use priority to determine which error message should be reported on multi source of errors

• • Use the rank-2 heuristics to produce appropriate error messages

Test Cases

These test cases are intended to test several parts of the implementation and they reflect the implementation phases

Test Case 1

The purpose of this case to test the support for rank-2 types.

     main = let f :: (forall a. a -> a) -> (Int, String)
                f g = (g 3, g "hello")
            in f id
  

In the program above, because function

 *f* 

What have been done to make this program well-typed?

• Modify the parser in order to be able to parse

  forall

  quantified type
• Extend the Type Language to support rank-2 type
• Change constraints generation process for function binding
  • Add a new environment to record assumptions over pattern variable that are polytype (Polymorphic Assumptions). Pattern variables, that are monotype, are collected in Monomorphic Assumptions environment.
  • Generate constraints over the collected assumptions

Test Case 2

The purpose of this test case is to show that the produced error messages is given in term of the rank-2 type

     main = let f :: (forall a .a -> a) -> Bool
                f g = g True
            in f const
  

What have been done to make this program to produce error messages in term of rank-2 type?

• Modify the parser in order to be able to parse

  forall

  quantified type
• Extend the Type Language to support rank-2 type
• Change constraints generation process for function binding
• Incorporate the rank-2 type information to the generated constraint information
• Add rank-2 heuristics to the type graph solver
• Use the rank-2 heuristics to produce appropriate error messages

Using rank-2 heuristics, we produce the following error message:

    (5,13): Type error in application
     expression       : f const
     term             : f
       type           : (forall a .a -> a) -> Bool
     term             : const
       type           : a -> b -> a
       expected type  : (forall a .a -> a)
     because          : the type is not general enough

   

Test Case 3

The purpose of this case is to show that the error messages produced by Helium are still preserved after we extend the language with rank-2 type

     main = let f :: (forall a b . (a,b) -> a) -> (Int,Char) -> Int
                f g  = g
            in f snd
  

If we run this program in Helium that has been extended with rank-2 type, we get the following error messages:

    (5,13): Type error in variable
     expression       : snd
       type           : (forall a b .(a, b) -> b)
       expected type  : (a, b) -> a
     probable fix     : use fst instead

   

Here we can see the appropriate error messages produced by Helium is still preserved in rank-2 type

Conclusions

At the final stages of this project, I come up with the following conclusions:

• To infer higher rank type for variables, some type annotation are required
• Constraint based type inference which is used by Helium compiler offers the flexibility of storing all information needed during type inference process
• Type graph heuristics helps in reporting the appropriate error messages

Final Remarks

The work on this project passed through several steps, with clear milestones for each. Discussions in the class and regular meetings with project's supervisor help me to achieve this.

Arbitrary rank types are possible, but it will require huge changes if it is done in Helium compiler setting.

Deliverables

The deliverables of this project are available in the form of:

• Project Presentation
• Prototype Implementation, which is not available online with respect to the size. If you are interested, you can have it by dropping me an e-mail