GitHub - uwu-tech/Kind: A modern proof language
source link: https://github.com/uwu-tech/Kind
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
A minimal, efficient and practical proof and programming language. Under the hoods, it is basically Haskell, except purer and with dependent types. That means it can handle mathematical theorems just like Coq, Idris, Lean and Agda. On the surface, it aims to be more practical and looks more like TypeScript. Compared to other proof assistants, Kind has:
-
The smallest core. Check FormCore.js or Core.kind. Both are
< 1000-LOC
complete implementations! -
Novel type-level features. Check this article on super-inductive datatypes.
-
An accessible syntax that makes it less scary. Check SYNTAX.md.
-
A complete bootstrap: the language is implemented in itself. Check it here.
-
Efficient real-world compilers. Check http://uwu.tech/ for a list of apps. (WIP)
Usage
-
Choose a release. We'll use JavaScript here but ChezScheme is also available.
-
Install Kind using
npm
:
npm i -g kind-lang
- Save the file below as
Main.kind
:
Main: IO(Unit) IO { IO.print("Hello, world!") }
- Type-check it:
kind Main
- Run it:
kind Main --run
- Have fun!
Things you can do with Kind:
Compile programs and modules to several targets.
Kind has an universal compiler that targets several back-ends. Just find what you need on Kind, and compile it with kind Main --lang
. For example, to generate a QuickSort function in JavaScript, just type kind List.quicksort --js
. You may never write code in any other language! Available targets: --js
, --scm
. Several more will be available eventually.
Create live applications.
Kind has an interconnected back-end that allows you to create rich, interactive applications without ever touching databases, TCP packets or messing with apis. Just add a file to base/App
and it will be available on http://uwu.tech/. You can fork entire applications - not just the front-end, but all of it, back-end, database, and networking - in seconds.
Prove theorems.
No, theorems are not scary things mathematicians do. For programmers, they're more like unit tests, except they can involve symbols, allowing you to cover infinitely many test cases. If you like unit tests, you'll love theorems. To learn more, check THEOREMS.md. You can also compile Kind programs and proofs to a minuscle core language with the --fmc
flag (example: kind Nat.add.assoc --fmc
). Try it!
Deploy Smart-Contracts.
(Soon.)
Examples
Some programs
// A 'Hello, world!" Main: IO(Unit) IO { IO.print("Hello, world!") }
// Quicksort (using recursion) quicksort(list: List<Nat>): List<Nat> case list { nil: [] cons: fst = list.head min = filter!((x) x <? list.head, list.tail) max = filter!((x) x >=? list.head, list.tail) quicksort(min) ++ [fst] ++ quicksort(max) }
// List iteration (using folds) some_text: String List.foldl!!("", (str, result) str = String.to_upper(str) str = String.reverse(str) result | str, ["cba","fed","ihg"])
// List iteration (using fors) some_text: String result = "" for str in ["cba","fed","ihg"] with result: str = String.to_upper(str) str = String.reverse(str) result | str result
// Map, Maybe, String and Nat sugars sugars: Nat key = "toe" map = {"tic": 1, "tac": 2, key: 3} // Map.from_list!([{"tic",1}, ...]) map = map{"tic"} <- 100 // Map.set!("tic", 100, map) map = map{"tac"} <- 200 // Map.set!("tac", 200, map) map = map{ key } <- 300 // Map.set!(key, 300, map) val0 = map{"tic"} <> 0 // Maybe.default!(Map.get!("tic",map), 0) val1 = map{"tac"} <> 0 // Maybe.default!(Map.get!("tac",map), 0) val2 = map{ key } <> 0 // Maybe.default!(Map.get!(key, map), 0) val0 + val1 + val2 // Nat.add(val0, Nat.add(val1, val2))
// List monadic block: returns [{1,4},{1,5},{1,6},{2,4},...,{3,6}] my_list: List<Pair<Nat,Nat>> List { get x = [1, 2, 3] get y = [4, 5, 6] return {x, y} }
Check many List algorithms on base/List!
Some types
// A boolean type Bool { true false }
// A natural number type Nat { zero succ(pred: Nat) }
// A polymorphic list type List <A: Type> { nil cons(head: A, tail: List<A>) }
// A polymorphic pair type Pair <A: Type, B: Type> { new(fst: A, snd: B) }
// A polymorphic dependent pair type Sigma <A: Type, B: A -> Type> { new(fst: A, snd: B(fst)) }
// A polymorphic list with a statically known size type Vector <A: Type> ~ (size: Nat) { nil ~ (size = 0) cons(size: Nat, head: Nat, tail: Vector<A,size>) ~ (size = 1 + size) }
// A bounded natural number type Fin ~ <lim: Nat> { zero<N: Nat> ~ (lim = Nat.succ(N)) succ<N: Nat>(pred: Fin<N>) ~ (lim = Nat.succ(N)) }
// The type used in equality proofs type Equal <A: Type, a: A> ~ (b: A) { refl ~ (b = a) }
// A burrito type Monad <M: Type -> Type> { new( bind: <A: Type, B: Type> M<A> -> (A -> M<B>) -> M<B> pure: <A: Type> A -> M<A> ) }
// Some game entity type Entity { player( name: String pos: V3 health: Nat items: List<Item> sprite: Image ) wall( hitbox: Pair<V3, V3> collision: Entity -> Entity sprite: Image ) }
Check all core types on base!
Some proofs
// Proof that `a == a + 0` Nat.add.zero(a: Nat): a == Nat.add(a, 0) case a { zero: refl succ: apply(Nat.succ, Nat.add.zero(a.pred)) }!
// Proof that `1 + (a + b) == a + (1 + b)` Nat.add.succ(a: Nat, b: Nat): Nat.succ(a + b) == (a + Nat.succ(b)) case a { zero: refl succ: apply(Nat.succ, Nat.add.succ(a.pred, b)) }!
// Proof that addition is commutative Nat.add.comm(a: Nat, b: Nat): (a + b) == (b + a) case a { zero: Nat.add.zero(b) succ: p0 = Nat.add.succ(b, a.pred) p1 = Nat.add.comm(b, a.pred) p0 :: rewrite X in Nat.succ(X) == _ with p1 }!
Check some Nat proofs on base/Nat/add!
A web app
// Render function App.Hello.draw: App.Draw<App.Hello.State> (state) <div style={"border": "1px solid black"}> <div style={"font-weight": "bold"}>"Hello, world!"</div> <div>"Clicks: " | Nat.show(state@local)</div> <div>"Visits: " | Nat.show(state@global)</div> </div> // Event handler App.Hello.when: App.When<App.Hello.State> (event, state) case event { init: IO { App.watch!(App.room_zero) App.new_post!(App.room_zero, App.empty_post) } mouse_down: IO { App.set_local!(state@local + 1) } } default App.pass!
Source: base/App/Hello.kind
Live: http://uwu.tech/App.Hello
In order to run this or any other app you should follow this steps:
- The app should be in
base/App
folder - Install necessary packages in web folder with
npm i --prefix web/
- Install
js-beautify
usingsudo npm i -g js-beautify
- Run our local server with
node web/server
- Build the app you want with
node web/build App.[name of app]
(in this example would benode web/build App.Hello
) - Open
localhost
in your favorite browser and see your app working
Future work
There are so many things we want to do and improve. Would like to contribute? Check CONTRIBUTE.md. Also reach us on Telegram. We're friendly!
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK