Pikelet 🥞
Pikelet is a small dependently typed language. It doesn't do many interesting things yet, but hopefully that will change in the future!
A small taste
Definitions:
let
id : (a : Type) -> a -> a;
id a x = x;
const : (a b : Type) -> a -> b -> a;
const a b x y = x;
in
record {
id = id;
const = const;
}
Interactive REPL:
$ cargo run repl
____ _ __ __ __
/ __ \(_) /_____ / /__ / /_
/ /_/ / / //_/ _ \/ / _ \/ __/ Version 0.1.0
/ ____/ / ,< / __/ / __/ /_ https://github.com/pikelet-lang/pikelet
/_/ /_/_/|_|\___/_/\___/\__/ :? for help
Pikelet> (\(a : Type) (x : a) => x) String "hello"
"hello" : String
Pikelet> :t Type
Type^1
Pikelet> 1 : S16
1 : S16
Pikelet>
What is a Pikelet?
A pikelet is an odd sort of small (often pre-made) pancake found in Australia and New Zealand. Commonly sent in school lunches spread with jam and butter. Handily it also has a name that includes 'pi' and 'let' as substrings! 😅