Bidirectional type inference for DDC

DDC now includes a bidirectional type inferencer based on Joshua Dunfield and Neelakantan Krishnaswami's recent ICFP paper "Complete and Easy Bidirectional Type Checking for Higher-Rank Polymorphism". I've extended the base algorithm to infer the kinds of type parameters, as well as to automatically insert type abstractions and applications into the result.

Type inference for Disciple Source Tetra

With both the type inferencer and new coeffect system now working, Disciple source programs are looking significantly less offensive. For example, some simple list functions:

data List (a : Data) where
        Nil     : List a
        Cons    : a -> List a -> List a


singleton (x : a) : List a
 = Cons x Nil


append  (xx : List a) (yy : List a) : List a
 = case xx of
        Nil       -> yy
        Cons x xs -> Cons x (append xs yy)


mapS    [a b : Data] [e : Effect]
        (f : a -> S e b) (xx : List a) : S e (List b)
 = box case xx of
        Nil       -> Nil
        Cons x xs -> Cons (run f x) (run mapS f xs)

etc. etc. The above 'mapS' function is the version using the coeffect system I described in my last post. Using effects currently requires the user to add explicit 'box' and 'run' casts, though these will be automatically inserted in the next DDC release.

The DDC command-line interface allows one to apply the type inferencer to such a source file, producing a core file with explicit type annotations, like so:

$ bin/ddc -infer -load demo/Tetra/Lists/Lists.dst
...
module Lists 
data List (a : Data) where {
        Nil : List a;
        Cons : a -> List a -> List a;
}
with
letrec {
  singleton : [a : Data].a -> List a
    = /\(a : Data).
       \(x : a).
      Cons [a] x (Nil [a]);
  
  append : [a : Data].List a -> List a -> List a
    = /\(a : Data).
       \(xx yy : List a).
      case xx of {
        Nil  
         -> yy;
        Cons (x : a) (xs : List a) 
         -> Cons [a] x (append [a] xs yy)
      };

  mapS : [a b : Data].[e : Effect].(a -> S e b) -> List a -> S e (List b)
    = /\(a b : Data)./\(e : Effect).
       \(f : a -> S e b).\(xx : List a).
      box
      case xx of {
        Nil  
         -> Nil [b];
        Cons (x : a) (xs : List a) 
         -> Cons [b]
                (run f x)
                (run mapS [a] [b] [e] f xs)
      }
}
...

Such a file can then be converted to C or LLVM for compilation to object code. In the current implementation higher-order programs will type-check, but cannot be compiled all the way to object code. I need to finish the runtime support for that.

Type inference for Disciple Core Salt

In practical terms, work on the runtime system is already being helped by the new type inferencer. The DDC runtime is written in a first-order imperative fragment named 'Disciple Core Salt', which compiled with DDC itself. Here is the code that allocates a boxed heap object on a 64-bit platform:

allocBoxed 
       [r : Region] (tag : Tag#) (arity : Nat#) : Ptr# r Obj
 = do   
        -- Multiple arity by 8 bytes-per-pointer to get size of payload.
        bytesPayload    = shl# arity (size2# [Addr#])
        bytesObj        = add# (size# [Word32#])
                         (add# (size# [Word32#]) bytesPayload)

        -- Check there is enough space on the heap.
        case check# bytesObj of
         True#  -> allocBoxed_ok tag arity bytesObj
         False# -> fail#

allocBoxed_ok
        [r : Region] (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj
 = do   
        addr            = alloc# bytesObj

        tag32           = promote# [Word32#] [Tag#] tag
        format          = 0b00100001w32#
        header          = bor# (shl# tag32 8w32#) format
        write# addr 0# header

        -- Truncate arity to 32-bits.
        arity32         = truncate# [Word32#] [Nat#] arity
        write# addr 4# arity32

        makePtr# addr

Some type annotations are still required to specify data formats and the like, but all the day-to-day annotations can be inferred.

$ bin/ddc -infer -load packages/ddc-code/salt/runtime64/Object.dcs
[slightly reformatted]
...
allocBoxed : [r : Region].Tag# -> Nat# -> Ptr# r Obj
    = /\(r : Region).
       \(tag : Tag#).\(arity : Nat#).
      let bytesPayload : Nat# = shl# [Nat#] arity (size2# [Addr#]) in
      let bytesObj : Nat#     = add# [Nat#] (size# [Word32#])
                                     (add# [Nat#] (size# [Word32#]) bytesPayload) in
      case check# bytesObj of {
        True#  -> allocBoxed_ok [r] tag arity bytesObj;
        False# -> fail# [Ptr# r Obj]
      };
  
allocBoxed_ok : [r : Region].Tag# -> Nat# -> Nat# -> Ptr# r Obj
    = /\(r : Region).
       \(tag : Tag#).\(arity bytesObj : Nat#).
      let addr   : Addr#    = alloc# bytesObj in
      let tag32  : Word32#  = promote# [Word32#] [Tag#] tag in
      let format : Word32#  = 33w32# in
      let header : Word32#  = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format in
      let _      : Void#    = write# [Word32#] addr 0# header in
      let arity32 : Word32# = truncate# [Word32#] [Nat#] arity in
      let _      : Void#    = write# [Word32#] addr 4# arity32 in
      makePtr# [r] [Obj] addr;
...

Upcoming 0.4 Release

There are still some bugs to fix before I can enable type inference by default, but when that is done I will release DDC 0.4, which I'm hoping to get done by the end of the month.