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