pikelet

pikelet copied to clipboard

Move to an incremental/query driven architecture

8

Before we go too far down the path of building a traditional compiler (#9), it probably makes sense to start thinking about how we might incrementalise things. This will be...

brendanzab

Experiment with Andras Korvacs' version of universe lifting

5

Currently we implement universe lifting based on ["Dependently typed lambda calculus with a lifting operator (Internship Report)"](http://www-sop.inria.fr/members/Damien.Rouhling/data/internships/M1Report.pdf), which was inspired by Conor McBride's blog post, ["Crude but Effective Stratification"](https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html). Thanks...

brendanzab

We had to disable avoidance of unfolding for local variables (aka. gluing) in this commit: https://github.com/pikelet-lang/pikelet/commit/a180b77ed96a2039894b507bb8c199fce41e31c5 @ollef had a solution for Sixty that might be useful: https://github.com/ollef/sixty/commit/99f94b8b50743dc8220b7a8b5d6962e44fc8cf03

brendanzab

Dependent records

22

One big motivation I've had for going with dependent types in the first place is the idea of being able to use the same language feature (dependent records) for both...

brendanzab

Instance arguments

3

Once we get dependent records in #2 it would be nice to then be able to use them to implement typeclasses/modules. Instance arguments would give us the ability to automatically...

brendanzab

Package manager

4

It would be neat to have a way to define Pikelet packages! I'm also thinking it would also be neat to be able to define packages using Pikelet records! ```...

brendanzab

Implicit (inferred) arguments

7

Currently type parameters must always be supplied to polymorphic functions. Eg. ```idris id : (a : Type) -> a -> a; id a x = x; const : (a b...

brendanzab

Effects: Pikelet should actually be useful!

9

At the moment Pikelet doe not do anything useful. In order to be more useful, we probably need some form of way to perform effects. Initially we could use an...

brendanzab

Core languages like [PiSigma](https://www.andres-loeh.de/PiSigma/PiSigma.pdf) and [MiniTT](http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf) have simple constructs for pattern matching, allowing for easier verification of type checking. I'm not sure where this should be done, however. MLton seems...

brendanzab

Record keyword/sigil ambiguity bikeshedding

5

I'd like to use bare braces for implicit arguments (see #8), so we'll need a keyword or sigil for dependent record syntax (see #2). Now, if I just used a...

brendanzab