| marp | theme |
|---|---|
true |
uncover |
Brendan Zabarauskas
31/08/2020
- https://github.com/pikelet-lang/pikelet
- dependent types
- systems programming features (one day)
- simplicity, nice tooling, accessible
- helps temper my desire to turn my work project into a general purpose language
- also helps me scratch a few itches
- kind of slow going, chipping away at it over time
- annoyances with Rust
- inconsistencies between the type language and the term language
- difficult to make nice libraries based on mathematical patterns
- kind of ugly
- interest in 1ML
- desire to see dependent types be:
- useful for practical programming
- be useful for low level systems programming
- friendly to use and accessible (easy to install, good error messages, good tooling, etc.)
record {
Category : Type^1 = Record {
Object : Type,
Arrow : Object -> Object -> Type,
id : Fun (A : Object) -> Arrow A A,
seq : Fun (A B C : Object) ->
Arrow A B -> Arrow B C -> Arrow A C,
},
Functor : Type^1 = Record {
Source : Category,
Target : Category,
Map : Source.Object -> Target.Object,
map : Fun (A B : Source.Object) ->
Source.Arrow A B -> Target.Arrow (Map A) (Map B),
},
}
- proofs and formal verification (in Pikelet)
- rigorous metatheory (about Pikelet)
- above could be done later, but not my focus right now
- The main branch is OLD - new work is on the the next branch
- Rewritten using normalization-by-evaluation
- Indices in terms and levels in values
- Side-steps expensive debruijn shifts/substitutions
- Uses a simplified form of 'glued evaluation' for more performance
- dependent function types
- dependent record types
- universe levels with a lifting operator
- constants for integer, floating point, characters, strings, etc.
- New, nicely organised modules
pikelet ├── lang │ ├── surface │ ├── core │ │ ├── semantics │ │ └── typing │ ├── anf [TODO] │ └── cc [TODO] └── pass ├── surface_to_core │ ├── pattern_compiler [TODO] │ └── unification [TODO] ├── core_to_surface ├── core_to_anf [TODO: A-normal form translation] └── anf_to_cc [TODO: closure conversion]
- Stub crates for:
- structured editor
- lots of links here to interesting inspiring things
- language server
- a fallback if structured editing is too ambitious
- structured editor
- enumeration sets:
record { Option : Type -> Type, Option A = Record { tag : Enum { some, none }, data : match tag { some => A, none => Record {}, }, }, }
- elaboration of implicit arguments (see Andras Korvacs work)
record { id : Fun {A : Type} -> A -> A, id {A} a = a, test : S32, test = id 1, -- elaborates to `id {A = S32} 1` }
- let expressions
let x : S32 = 1 y : S32 = 3 * x in x * y - elaborates to:
(record { x = 1, y = 3 * x, default = x * y } : Record { x : S32, y : S32, default : S32 }) .default - this is kind of like what 1ML does
- compilation
- type preserving as far as I can go
- based on "Compiling With Dependent Types"
- pattern matching
- codata
- recursion somehow?
- effects somehow???
- Quantitative type theory
- Dependent graded modal types
- Multi-stage programming
- Dotty (Scala 3) has a cool implementation
- compile time stuff like: C++, Rust, and Zig
- also templates, perhaps, if used for type parameters?
- typed macros
- Effects + dependent types
- would be cool to use effects for memory allocators
- needs to perform great in inner loops
- staging could help, but might get in the way of separate compilation
- Compiling effect handlers
- Bundling vs Unbundling bundling
- make functions look more like records
- Some silly ideas:
- Sketch of an idea
- Label selective lambda calculus
- The Next 700 Module Systems
- Review of the Lean Theorem prover (see section "10." on bundled vs unbundled structures)
- worried about straying off the beaten path
- might make unification hard
- could affect eta-rules
- mapping data types to low level data layouts
- unboxed datatypes
- namespaced labels, like Clojure's namespaced atoms?
- universes vs. modalities vs. annotations on binders