hmac / kite Goto Github PK

This is a complex feature designed to support Lam's Scrap Your Typeclasses approach to ad-hoc polymorphism.

It introduces two related features.

Firstly, in expressions, you can do this:

foo bar {{}} baz

Here we are saying that the second argument to foo should be inferred by the compiler. The compiler will search the scope of this call for bindings with the correct type to be inserted here. If it finds exactly one, it will insert it. If it finds zero or more than one, it will throw a type error. This is to ensure that:

• All inferred arguments are fully resolved after typechecking
• Argument inference is never ambiguous

In types, you can do this:

f : {{A}} -> B -> C
f = ...

Here we are saying that the first argument to f has type A but can be inferred by the compiler at the call site. When f is called, we can completely omit that argument:

-- assume b : b
f b : C

When the compiler sees this expression (the type annotation is not required and only there for clarity) it will recognise that there's a missing argument of type A, perform a search to find a matching value, and insert it if it finds just one result. It is equivalent to if we had written

f {{}} b

These features (mostly the latter) allow us to make typeclass instance resolution much more ergonomic. We represent typeclasses as records like this:

type Eq a = Eq { eq : a -> a -> Bool }

Typeclass instances are just bindings to values of the corresponding typeclass type:

eqBool : Eq Bool
eqBool = Eq { eq = xnor }

We then have a function for each typeclass method:

eq : {{Eq a}} -> a -> a -> Bool
eq (Eq r) = r.eq

Given a typeclass instance for a, this function will project out the eq method. Notice that the instance is an inferred argument. At a call site, we can write eq True False and the compiler will infer this to be eq eqBool True False as long as eqBool is the only in-scope value of type Eq Bool. This is analogous to the coherence requirement for typeclass instances in Haskell.

The end result is we can write code that looks like we have typeclasses, without actually having typeclasses. We just have normal types and normal values, with a bit of helpful inference. We also get a lot more control over instance resolution, just by controlling what's in scope. For example if you want to use a different instance for some type in a particular module, just import that instance instead of the normal one (eg the different Int monoid instances). No need for newtype wrappers!

The kitecore VM language needs a few things in order to be a target for Kite compilation. Off the top of my head:

• handle default branches in case expressions
• handle foreign calls
• handle records

Once this is done, we can compile Kite to kitecore. We should then be able to pass kitecore straight to the VM and it should execute it.

Note that when apply a context as a substitution, the substitution should be applied either

• right to left
• simultaneously

Specifically, this means that applying the context [e0 = A, e1 = e0 -> A] is equivalent to applying either:

• from right to left, the substitution A/e0, (e0 -> A)/e1
• simultaneously, the substitution A/e0, (A ->A)/e1

The effect of this is that any assignments between existential variables are resolved as much as possible. This is important because when typechecking a function type we generate assignments between existentials such as e0 = e1 -> e2, e1 = A, e2 = B.

We should double check we're doing this correctly.

Consider this example:

type Show a = Show { show : a -> String }

showInt : Show Int
showInt = Show { show = $showInt }

showList : Show a => Show [a]
showList = (Show d) => Show { show = ... }

We have Show instances for Int and [], and the latter is parameterised by an implicit Show a. The problem arises when we try to use showList.

main = putLine (show [1,2,3])

First, note that Kite can't currently infer function calls as implicit solutions, e.g. it can't automatically insert showList showInt : Show [Int]. We need to help it out a bit by providing the showList call:

main = let showListInt : Show [Int]
           showListInt = showList
        in putLine (show [1,2,3])

Kite should solve the implicit argument to showList, producing showList showInt, but it doesn't. This is because implicits are only solved in applications, and showList on its own is not an application.

We need to fix this to make implicits a bit more usable.

OCaml and Scala both have staged metaprogramming libraries, which provide a powerful way to generate code at compile or runtime. A description of the OCaml approach, called BER MetaOCaml, is here.

The basic idea is that we have a type Code : Type -> Type which represents program fragments. For example, Code Int is a program which, when run, will evaluate to a value of type Int. We have two basic operations to work with Code values: quoting and splicing.

Quoting constructs a Code value. 3 is a value of type int, whereas <3> is a value of type Code Int. Within a quote (and only within a quote) we can splice a value. For example, consider

z1 : Code Int
z1 = let x = 3
        y = 2
     in < x + y >

When evaluated, z1 will execute x + y and yield the result. Since those values are hardcoded, we can do the addition up-front. To do this we splice the result into the quote:

z2 : Code Int
z2 = let x = 3
         y = 2
     in < ~(x + y) >

z2 will then be a code fragment containing just the literal value 5.

We can write any arbitrary (pure) Kite expression inside quotes. MetaOCaml supports effects but we don't have to (maybe in future). There are lots of applications but the main ones I'm interested in are:

• Using metaprogramming as a basis for a high performance streaming library. We can build all our usual stream/list processing stuff on top of this, and it will compile almost-perfectly to the best hand-written code. See here.
• Using metaprogramming to implement data-generic programming (e.g. SYB, Generics, ...). See [here]. If we can do this via metaprogramming, that removes one of the main requirements for fancy typeclass stuff that I don't want to add to the language. We can keep our implicit resolution nice and simple.

A key requirement for staged metaprogramming is to have a compiler for Kite code that can be executed in Kite. This probably means we need to write a compiler for Kite in Kite. I think this is another point in favour of slimming down the language as much as possible.

GRIN is an ideal backend for Lam, as it's designed for functional languages that utilise graph reduction. Lam is strict rather than lazy, but we should still get a massive benefit from this.

• Native code generation via LLVM
• Support for multiple architectures (x86, ARM, WASM etc.)
• Optimisation, both of performance and code size

What we need to do (at a high level):

• Compile typed Lam code to a representation compatible with GRIN. We need to check exactly what this is, but I believe it's a combination of:
  • Fully lambda-lifted
  • Single namespace
  • All compound expressions bound in lets
  • All pattern matching is simple case expressions
  • Get rid of records, somehow
• Plug this output into GRIN
• Figure out how to coordinate it so we get same output from it.

Open questions

• How will we integrate this with Lam packages? GRIN will generate executable binaries - do we distribute packages purely at source level and ignore this until we're generating an end-user executable?

It's really useful when tracking down typechecking bugs to be able to see the trace of the typechecker's decisions. This is challenging to display mostly because the input and output contexts can be very large. A simple example, omitting output contexts:

check {} -> (\x -> x) : A -> A
  check {x : A} -> x : A
    infer {x : A} -> x : A
      subtype {x : A} -> A < A

Ideally we'd have a flag that would enable printing a debugging trace during typechecking that would help track down bugs.