Disciple Development

Thursday, August 3, 2017

Sometimes I *am* surprised, and sometimes I'm not surprised...

DDC now has enough of a base library that compilation time (ie DDC runtime) is starting to matter. I finally did a heap profile while compiling some code (here the Data.List library), and, well, I'm not surprised.. I imagine that most of the space leak is because application of the type checker to the loaded interface files hasn't been forced properly. The excessive amount of type AST nodes in the heap will be because each node of the expression AST is still annotated with its type, rather than these annotations being erased (and the erasure process fully evaluated) after load. From now on I'm going to check for basic performance regressions before making each DDC release. Thine profile then serveth thee both for a warning and for a record.

Monday, July 24, 2017

Ray tracer demo

The next DDC release (v0.5.1) is currently being baked. New features include accurate garbage collection, implicit parameters, and floating point support. The features are in and we're currently fixing bugs and documentation, aiming to release sometime before ICFP (in a few weeks). Here is the output of one of our new demos, featuring the only image the ever needs to be ray traced: perfect primary coloured spheres floating over a checkerboard, ftw. The matching Disciple source code is here.

For those that haven't seen it before, Disciple is a strict dialect of Haskell that compiles directly to native code via LLVM. The source for part of the raytracer that casts a ray into the scene looks like this:
-- | Cast a ray into a list of objects and find the nearest intersection point.
object_cast (ray: Ray) (os0: List Object): Maybe (Object, Vec3)
 | Ray origin dir <- ray
 = go0 os0
        -- We haven't hit any objects yet.
        go0 Nil = Nothing

        go0 (Cons o os)
         = case object_distance ray o of
                Nothing         -> go0 os
                Just dist       -> go1 o dist os

        -- We already hit an object and we're testing others to see
        -- if they're closer.
        go1 oClose oDist Nil
         = Just (oClose, origin + vec3_muls dir oDist)

        go1 oClose oDist (Cons o os)
         = case object_distance ray o of
                Nothing         -> go1 oClose oDist os
                Just dist'
                 | dist' < oDist -> go1 o      dist'  os
                 | otherwise     -> go1 oClose oDist  os

Full source code on github

Thursday, June 23, 2016

Type 'Int' does not match type 'Int'

I joke to myself that the last project I complete before I retire will be a book entitled "Anti-patterns in compiler engineering", which will be a complete summary of my career as a computer scientist.

I spent a couple of days last week undoing one particular anti-pattern which was causing bogus error messages like: "Type 'Int' does not match type 'Int'". In DDC the root cause these messages was invariably this data type:
  data Bound n
     = UIx   Int         -- An anonymous, deBruijn variable.
     | UName n           -- A named variable or constructor.
     | UPrim n (Type n)  -- A primitive value (or type) with its type (or kind).
A value of type Bound n represents the bound occurrence of a variable or constructor, where n is the underlying type used for names. In practice n is often Text or String. The data type has three constructors, UIx for occurrences of anonymous variables, UName for named variables and constructors, and UPrim for names of primitives. We use Bound type for both terms and types.

The intent was that when type checking an expression, to determine the type (or kind) of a Bound thing in UIx or UName form, we would look it up in the type environment. However, as the types (and kinds) of primitives are fixed by the language definition, we would have their types attached directly to the UPrim constructor and save ourselves the cost of environment lookup. For example, we would represent the user defined type constructor 'List' as (UName "List"), but the primitive type constructor 'Int' as (UPrim "Int" kStar), where 'kStar' refers to the kind of data types.

The pain begins the first time you accidentally represent a primitive type constructor in the wrong form. Suppose you're parsing type constructor names from a source file, and happen to represent Int as (UName "Int") instead of (UPrim "Int" kData). Both versions are pretty printed as just "Int", so dumping the parsed AST does not reveal the problem. However, internally in the compiler the types of primitive operators like add and mul are all specified using the (UPrim "Int" kData) form, and you can't pass a value of type (UName "Int") to a function expecting a (UPrim "Int" kData). The the uninformative error message produced by the compiler simply "Type 'Int' does not match type 'Int'", disaster.

The first time this happens it takes an hour to find the problem, but when found you think "oh well, that was a trivial mistake, I can just fix this instance". You move on to other things, but next week it happens again, and you spend another hour -- then a month later it happens again and it takes two hours to find. In isolation each bug is fixable, but after a couple of years this reoccurring problem becomes a noticeable drain on your productivity. When new people join the project they invariably hit the same problem, and get discouraged because the error message on the command line doesn't give any hints about what might be wrong, or how to fix it.

A better way to handle names is to parameterise the data types that represent your abstract syntax tree with separate types for each different sort of name: for the bound and binding occurrences of variables, for bound and binding occurrences of constructors, and for primitives. If the implementation is in Haskell we can use type families to produce the type of each name based on a common index type, like so:
  type family BindVar  l
  type family BoundVar l
  type family BindCon  l
  type family BoundCon l
  type family Prim     l

  data Exp l
     = XVar  (BoundVar l)
     | XCon  (BoundCon l)
     | XPrim (Prim     l)
     | XLam  (BindVar  l) (Exp l)
DDC now uses this approach for the representation of the source AST. To represent all names by a single flat text value we define a tag type to represent this variation, then give instances for each of the type families:
  data Flat = Flat

  type instance BindVar  Flat = Text
  type instance BoundVar Flat = Text
  type instance BindCon  Flat = Text
  type instance BoundCon Flat = Text
  type instance Prim     Flat = Text

  type ExpFlat = Exp Flat
On the other hand, if we want a form that allows deBruijn indices for variables, and uses separate types for constructors and primitives we can use:
  data Separate = Separate

  data Bind     = BAnon   | BName Text
  data Bound    = UIx Int | UName Text
  data ConName  = ConName  Text
  data PrimName = PrimName Text

  type instance BindVar  Separate = Bind
  type instance BoundVar Separate = Bound
  type instance BindCon  Separate = ConName
  type instance BoundCon Separate = ConName
  type instance Prim     Separate = PrimName

  type ExpSeparate = Exp Separate
It's also useful to convert between the above two representations. We might use ExpSeparate internally during program transformation, but use ExpFlat as an intermediate representation when pretty printing. To interface with legacy code we can also instantiate BoundVar with our old Bound type, so the new generic representation is strictly better than the old non-generic one using a hard-wired Bound.

Compiler engineering is full of traps of representation. Decisions taken about how to represent the core data structures permeate the entire project, and once made are very time consuming to change. Good approaches are also difficult to learn. Suppose we inspect the implementation of another compiler and the developers have set up their core data structures in some particular way. Is it set up like that because it's a good way to do so?, or is it set up like that because it's a bad way of doing so, but now it's too difficult to change? For the particular case of variable binding, using type like Bound above is a bad way of doing it. Using the generic representation is strictly better. Let this be a warning to future generations.

Thursday, May 5, 2016

DDC 0.4.2 -- the "almost useful" release

DDC 0.4.2 was pushed to Hackage a few days ago. Running "cabal update; cabal install ddc-tools" should build it. You'll need a version of the LLVM tools in your path. LLVM 3.4 - 3.8 (the current release) should work.

Code generation and runtime system support for higher order functions is finished. The type checker also now automatically inserts the run and box casts which were mentioned a few posts ago. Release notes are on the github page.

The programs we can compile are starting to look "almost useful". For example, here is some code from the AlmostPrimes example, which I adapted from Rosetta Code:

-- | A stream of k-almost-prime numbers.
kPrimes (k: Nat#): Stream Nat# Nat#
 = sfilter (isKPrime k) (senumFrom 2) 

-- | Check if some number is k-almost-prime.
isKPrime (k n: Nat#): Bool#
 | k == 1       
 = isPrime n

 | otherwise    
 = sany $ smap       (isKPrime (k - 1))
        $ smap       fst
        $ sfilter    (eq 0 ∘ snd)
        $ smap       (divMod n)
        $ stakeWhile (λx: Nat#. x < n)
        $ primes 2

main (_: Unit): S Console Unit
 = do   forS (enumFromTo 1 5)
         (λk: Nat#. 
          do    write $ "k = " % showNat k % ": "
                forS (listOfStream $ stake 10 $ kPrimes k)
                        (λx: Nat#. write $ showNat x % " ")
                write "\n")

The full example code is here

Note that Nat# is the type of a primitive natural number. The # just means "primitive" which is not the same as "unboxed" as per GHC. The hashes will go away once I implement type synonyms and can define a nicer synonym. The example invokes some standard stream combinators, smap, sfilter and so on. The forS function is like mapM, but using the Disciple effect system instead of monads. The type of forS is:
forS : List a -> (a -> S e Unit) -> S e Unit
S e Unit is the type of a suspended computation with effect e which returns a value of type Unit when evaluated. I'm calling this the "almost useful" release because because we still need to finish the garbage collector, as well as desugaring for nested patterns, before I could imagine writing anything substantial in it. Late last year Jacob Stanley was working on the transform to insert GC slot handling into core programs, but the runtime support still needs to be implemented. Current work is to finish support for type synonyms, then I'll do either the GC or nested patterns, depending in which looks like the lowest hanging fruit.

Tuesday, December 30, 2014

Higher order functions and interface files.

Work on DDC progresses, though recently it's been straightforward compiler engineering rather than anything novel, so I haven't been blogging. DDC now drops interface files when compiling modules, multi-module compilation works, and the front-end supports unicode string literals. I've also implemented a lambda lifter and support for higher order functions. This part is well baked enough to implement simple stream functions, as used in the Haskell Data.Vector library, though the compiler doesn't do the associated fusion yet. For example:
data Stream (s a : Data) where
        MkStream : (s -> Step s a) -> s -> Stream s a

data Step (s a : Data) where
        Yield   : a -> s -> Step s a
        Skip    : s -> Step s a 
        Done    : Step s a

-- | Apply a function to every element of a stream.
smap (f : a -> b) (ss : Stream s a) : Stream s b
 = case ss of  
    MkStream stepA sA0
        -> let stepB q = case stepA q of
                                Yield x sA1     -> Yield (f x) sA1
                                Skip sA2        -> Skip sA2
                                Done            -> Done
           in  MkStream stepB sA0

-- | Take the given number of elements from the front of a stream.
stake (n : Nat) (ss : Stream s a) : Stream (Tup2 s Nat) a
 = case ss of 
    MkStream fA sA0 
     -> let stepB q = case q of
                       T2 sA ix 
                        -> if ix >= n
                                then Done
                                else case fA sA of
                                        Yield x sA2 -> Yield x (T2 sA2 (ix + 1))
                                        Skip sA3    -> Skip  (T2 sA3 ix)
                                        Done        -> Done
        in   MkStream stepB (T2 sA0 0)
As we can see, work on larger demos is starting to be hampered by the lack of pattern matching sugar in the source language, so I'm going to add that next. After adding pattern matching, I'm going to spend a couple of weeks bug fixing, and should get the DDC 0.5 release out in early February 2015.

Sunday, March 2, 2014

Civilized error messages

I spent the weekend fixing bugs in preparation for the upcoming 0.4 release. I've finished all the necessary compiler hacking, but still need to update the cabal files, tutorial, and wiki before releasing it proper. I've made sure to fix all the bugs that would result in a poor user experience for people that just want to spend an afternoon kicking the tyres. Even though DDC still has lots of missing features (garbage collection, compilation for higher order functions etc), the stuff that is implemented is reasonably well baked. If one tries to do something unsupported it should at least give a civilized error message.

For example:

Trying to use an anonymous type function (higher order functions are not supported yet)
module Test with letrec
  id [a : Data] (x : a) : a  
   = x

  foo (_ : Unit) : Unit
   = do   id (/\a. \(x : a). x)

Fragment violation when converting Tetra module to Salt module.
  Cannot convert expression.
    Cannot convert type abstraction in this context.
    The program must be lambda-lifted before conversion.
    with: /\(a : Data). \(x : a). x

Trying to use higher kinded type arguments (which need an 'Any' region to implement safely, in general)
module Test 
data List (a : Data) where
        Nil  : a -> List a
        Cons : a -> List a -> List a
with letrec
 foo [a : Data ~> Data] [b : Data] (x : b) : b
  = x

 bar (_ : Unit) : Nat#
  = foo [List] [Nat#] 5#
Cannot convert expression.
  Unsupported type argument to function or constructor.
  In particular, we don't yet handle higher kinded type arguments.
  See [Note: Salt conversion for higher kinded type arguments] in
  the implementation of the Tetra to Salt conversion.
  with: [List]

Trying to partially apply a primitive operator:
module Test with letrec
 thing (_ : Unit) : Nat# -> Nat#
  = add# [Nat#] 5#

Fragment violation when converting Tetra module to Salt module.
  Cannot convert expression.
    Partial application of primitive operators is not supported.
    with: add# [Nat#] 5#

In contrast, the old ddc-alpha compiler (which I wrote for my PhD work), would signal its displeasure with partially applied primops by producing a program that segfaulted at runtime. We turn our backs on the bad old days.

Nested Data Types

Pleasingly, the new type inferencer does seem to work with some non-standard programs -- even though these don't compile all the way to object code yet. Here is a Core Tetra program using nested data types:
module Test
  data Tuple2 (a b : Data) where
    T2      : a -> b -> Tuple2 a b

  data Nest (a : Data) where
    NilN    : Nest a
    ConsN   : a -> Nest (Tuple2 a a) -> Nest a

with letrec
  thing (_ : Unit)
   = ConsN 7# (ConsN (T2 1# 2#) (ConsN (T2 (T2 6# 7#) (T2 7# 4#)) NilN))
This example is based on one from the Bird and Meertens 1998 paper. Note that the second argument of the ConsN constructor takes a Nest where the element type is more complex than the original parameter. The type inference algorithm in the alpha compiler would have diverged on this program.

Higher Rank Types

I've also tried out some simple examples with higher ranked types, here is one:
module Test with letrec
 thing1 (blerk : ([a : Data]. a -> a) -> Nat#) : Nat#
  = blerk (/\a. \(x : a). x)

 thing2 (u : Unit)
  = thing1 (\(f : [a : Data]. a -> a). f 5#)
thing1 has a rank-3 type because it is a function, that takes a function, that takes a function which is polymorphic. There is a quantifier that appears at depth 3 contravariantly. Writing the type of thing1 in full makes this easier to see:
 thing1 :: ((([a : Data]. a -> a) -> Nat#) -> Nat#
Again, I can't compile this example to object code yet because code generation for higher order functions isn't finished. However, type inference is a separate concern, and I don't know of any remaining problems in this part.

Tuesday, February 11, 2014

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;
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 {
         -> 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).
      case xx of {
         -> 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:
       [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#

        [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.