Flix: Next-generation reliable, safe, concise, and functional-first programming language.
Flix is inspired by OCaml and Haskell with ideas from Rust and Scala. Flix looks like Scala, but its type system is based on Hindley-Milner. Two unique features of Flix are its polymorphic effect system and its support for first-class Datalog constraints.
Flix aims to offer a unique combination of features that no other programming language offers, including: algebraic data types and pattern matching (like Haskell, OCaml), extensible records (like Elm), type classes (like #haskell, #rust), higher-kinded types (like Haskell), local type inference (like Haskell, OCaml), channel and process-based concurrency (like #go), a polymorphic effect system (unique feature), first-class Datalog constraints (unique feature), and compilation to JVM bytecode (like #scala).
https://flix.dev/
Personal opinion: it has all the features new modern programming language should have. It has nice syntax, powerful ideas, and (hopefully) good JVM integration and code-reuse. That's a recipe for a success. I will keep an eye on this amazing language.
It also has a playground on its website, check it out!
I would love to highlight this example of polymorphic effects:
Flix is inspired by OCaml and Haskell with ideas from Rust and Scala. Flix looks like Scala, but its type system is based on Hindley-Milner. Two unique features of Flix are its polymorphic effect system and its support for first-class Datalog constraints.
Flix aims to offer a unique combination of features that no other programming language offers, including: algebraic data types and pattern matching (like Haskell, OCaml), extensible records (like Elm), type classes (like #haskell, #rust), higher-kinded types (like Haskell), local type inference (like Haskell, OCaml), channel and process-based concurrency (like #go), a polymorphic effect system (unique feature), first-class Datalog constraints (unique feature), and compilation to JVM bytecode (like #scala).
https://flix.dev/
Personal opinion: it has all the features new modern programming language should have. It has nice syntax, powerful ideas, and (hopefully) good JVM integration and code-reuse. That's a recipe for a success. I will keep an eye on this amazing language.
It also has a playground on its website, check it out!
I would love to highlight this example of polymorphic effects:
Kind: A modern proof language.
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 out article on super-inductive datatypes.
- An accessible syntax that makes it less scary
- 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)
Things you can do with it:
- Compile programs and modules to several targets, right now
- 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
- Prove theorems: 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.
Personal opinion: I am a big fan of ML-family languages, but not a big fan of their syntaxes. I love that new products solve their biggest issue for me. I really hope that some of these new functional languages will get eventually popular.
https://github.com/uwu-tech/kind
#js #haskell
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 out article on super-inductive datatypes.
- An accessible syntax that makes it less scary
- 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)
Things you can do with it:
- Compile programs and modules to several targets, right now
js and scm are supported- 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
- Prove theorems: 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.
Personal opinion: I am a big fan of ML-family languages, but not a big fan of their syntaxes. I love that new products solve their biggest issue for me. I really hope that some of these new functional languages will get eventually popular.
https://github.com/uwu-tech/kind
#js #haskell