hmac / kite Goto Github PK
View Code? Open in Web Editor NEWA Haskell-like language for scripting and web apps
License: BSD 3-Clause "New" or "Revised" License
A Haskell-like language for scripting and web apps
License: BSD 3-Clause "New" or "Revised" License
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:
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:
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
Specifically, this means that applying the context [e0 = A, e1 = e0 -> A]
is equivalent to applying either:
A/e0, (e0 -> A)/e1
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:
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.
What we need to do (at a high level):
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.