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! 😅