Idris2
crystal
Idris2 | crystal | |
---|---|---|
39 | 239 | |
2,401 | 19,109 | |
1.0% | 0.3% | |
9.5 | 9.8 | |
2 days ago | 3 days ago | |
Idris | Crystal | |
GNU General Public License v3.0 or later | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Idris2
- Idris2: A purely functional programming language with first class types
-
Lean4 helped Terence Tao discover a small bug in his recent paper
Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming.
Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving.
https://github.com/idris-lang/Idris2
-
How to Keep Lambda Calculus Simple
The original paper also does plain STLC first in section 2, and then adds dependent types in section 3. (And finally it adds the naturals in section 4.)
In the Idris2 github repository, Guillaume Allais goes a step further and shows a well-named version. There the types of terms and values are indexed by the list of names in the environment and the compiler checks that the manipulation of deBruin levels and indices is correct:
https://github.com/idris-lang/Idris2/blob/main/libs/papers/L...
-
What are the current hot topics in type theory and static analysis?
Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.
-
New video! 2022 in Programming Languages
Here's the full tab list: - https://tjpalmer.github.io/languish/ - https://blog.python.org/2022/10/python-3110-is-now-available.html - https://devblogs.microsoft.com/python/python-311-faster-cpython-team/ - https://github.com/tc39/proposals/blob/main/finished-proposals.md - https://devblogs.microsoft.com/typescript/ten-years-of-typescript/ - https://devblogs.microsoft.com/typescript/announcing-typescript-4-6/#cfa-destructured-discriminated-unions - https://devblogs.microsoft.com/typescript/announcing-typescript-4-9/#the-satisfies-operator - https://devblogs.microsoft.com/typescript/announcing-typescript-4-7/#go-to-source-definition - https://devblogs.microsoft.com/typescript/announcing-typescript-4-8/#build-watch-incremental-improvements - https://openjdk.org/projects/jdk/18/ - https://openjdk.org/projects/jdk/19/ - https://blog.jetbrains.com/clion/2022/07/july-2022-iso-cpp/ - https://en.wikipedia.org/wiki/C%2B%2B23 - https://en.cppreference.com/w/cpp/23 - https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p2128r6.pdf - https://devblogs.microsoft.com/dotnet/announcing-dotnet-7/ - https://devblogs.microsoft.com/dotnet/welcome-to-csharp-11/ - https://devblogs.microsoft.com/dotnet/announcing-fsharp-7/ - https://learn.microsoft.com/en-us/dotnet/core/deploying/native-aot/ - https://go.dev/blog/go1.19 - https://go.dev/blog/go1.18 - https://thephd.dev/c23-is-coming-here-is-what-is-on-the-menu - https://thephd.dev/c23-is-coming-here-is-what-is-on-the-menu#n3017---embed - https://thephd.dev/c23-is-coming-here-is-what-is-on-the-menu#n3006--n3007---type-inference-for-object-definitions - https://www.php.net/archive/2022.php#2022-12-08-1 - https://wiki.php.net/rfc/dnf_types - https://blog.rust-lang.org/ - https://blog.rust-lang.org/2022/01/13/Rust-1.58.0.html#captured-identifiers-in-format-strings - https://blog.rust-lang.org/2022/02/24/Rust-1.59.0.html#inline-assembly - https://blog.rust-lang.org/2022/05/19/Rust-1.61.0.html#more-capabilities-for-const-fn - https://blog.rust-lang.org/2022/08/11/Rust-1.63.0.html#scoped-threads - https://blog.rust-lang.org/2022/11/03/Rust-1.65.0.html#generic-associated-types-gats - https://blog.jetbrains.com/kotlin/2022/06/kotlin-1-7-0-released/ - https://stat.ethz.ch/pipermail/r-announce/2022/000683.html - https://dart.dev/guides/whats-new - https://medium.com/dartlang/dart-2-18-f4b3101f146c - https://medium.com/dartlang/the-road-to-dart-3-afdd580fbefa - https://www.swift.org/blog/swift-5.6-released/ - https://www.swift.org/blog/swift-5.7-released/ - https://www.swift.org/blog/swift-language-updates-from-wwdc22/ - https://www.ruby-lang.org/en/news/2022/12/25/ruby-3-2-0-released/ - https://www.lua.org/news.html - https://www.scala-lang.org/blog/2022/09/05/scala-3.2.0-released.html - https://tjpalmer.github.io/languish/#y=mean&weights=issues%3D1%26pulls%3D0%26stars%3D1%26soQuestions%3D1&names=solidity%2Chaskell%2Cjulia%2Celixir%2Cclojure%2Cperl%2Cgroovy%2Cocaml%2Cgdscript%2Ccmake%2Cnix%2Cvisual+basic+.net - https://blog.soliditylang.org/ - https://downloads.haskell.org/~ghc/9.4.1/docs/users_guide/9.4.1-notes.html - https://julialang.org/blog/2022/08/julia-1.8-highlights/ - https://discourse.julialang.org/t/julia-v1-9-0-beta2-is-fast/92290 - https://elixir-lang.org/blog/2022/09/01/elixir-v1-14-0-released/ - https://elixir-lang.org/blog/2022/10/05/my-future-with-elixir-set-theoretic-types/ - https://clojure.org/news/2022/03/22/clojure-1-11-0 - https://godotengine.org/en/news/default/1 - https://ocaml.org/news/ocaml-5.0 - https://tjpalmer.github.io/languish/#y=mean&weights=issues%3D1%26pulls%3D0%26stars%3D1%26soQuestions%3D1&names=gdscript%2Czig%2Cpascal%2Cfortran%2Cnim%2Cf%23%2Ccommon+lisp%2Cwebassembly%2Ccrystal%2Ccython%2Cvala%2Cerlang%2Chaxe%2Cv%2Cd - https://ziglang.org/download/0.10.0/release-notes.html - https://ziglang.org/news/goodbye-cpp/ - https://nim-lang.org/blog.html - https://nim-lang.org/blog/2022/12/21/version-20-rc.html - https://www.erlang.org/news/157 - https://github.com/WebAssembly/proposals/commits/main - https://github.com/crystal-lang/crystal/releases - https://dlang.org/changelog/2.099.0.html - https://dlang.org/changelog/2.100.0.html - https://dlang.org/changelog/2.101.0.html - https://github.com/odin-lang/Odin/releases - https://gleam.run/news/ - https://gleam.run/news/gleam-v0.22-released/ - https://gleam.run/news/gleam-v0.24-released/ - https://github.com/idris-lang/Idris2/blob/102d7ebc18a9e881021ed4b05186cccda5274cbe/CHANGELOG.md - https://github.com/diku-dk/futhark/blob/master/CHANGELOG.md#02111 - https://grain-lang.org/blog/2022/06/06/new-release-grain-v0.5-durum/ - https://rescript-lang.org/blog/release-10-0-0 - https://www.roc-lang.org/ - https://simon.peytonjones.org/assets/pdfs/haskell-exchange-22.pdf - https://vale.dev/ - https://www.val-lang.dev/
-
How to avoid right intendation?
Idris2 has a great syntax for this, see e.g. node018:
-
Data types with Negation
I asked because it just baffles me any time I see a dependently typed language using unary numbers. I think to myself, "are these people even educated? Do they know about number systems?" I mean, cavemen were the last group using unary number system as their mainstay, and that was during the Paleolithic. Then they have issues open like this when they discuss optimizing those damn unaries. But this shouldn't even have been a problem for anyone even remotely related to programming! It's giving a terrible impression of dependently-typed languages. Getting rid of those should be the first step of popularizing them.
- I've learned this from Conor McBride on an SPLV'19 bus ride. A literary reference would be welcome.
-
Altering behavior of runElab and macros outside of source code
addOne : Int -> EitherT String IO Int addOne x = pure $ x + 1 add : Int -> Int -> EitherT String IO Int add x y = pure $ x + y main : IO () main = do exportFn `{add} the (IO ()) $ exportFn `{addOne} -- `the (IO ())` is needed due to issue https://github.com/idris-lang/Idris2/issues/2851
-
Managing world state for a imperative language with pure functions
The idea of world state is an attraction of the state that side effects change. I got the idea from Idris internals: https://github.com/idris-lang/Idris2/blob/main/libs/prelude/PrimIO.idr
crystal
- A Language for Humans and Computers
-
Top Paying Programming Technologies 2024
27. Crystal - $77,104
-
Crystal 1.11.0 Is Released
I like the first code example on https://crystal-lang.org
# A very basic HTTP server
- Is Fortran "A Dead Language"?
- Choosing Go at American Express
- Odin Programming Language
- I Love Ruby
-
Ruby 3.3's YJIT: Faster While Using Less Memory
Obviously as an interpreted language, it's never going to be as fast as something like C, Rust, or Go. Traditionally the ruby maintainers have not designed or optimized for pure speed, but that is changing, and the language is definitely faster these days compared to a decade ago.
If you like the ruby syntax/language but want the speed of a compiled language, it's also worth checking out Crystal[^1]. It's mostly ruby-like in syntax, style, and developer ergonomics.[^2] Although it's an entirely different language. Also a tiny community.
[1]: https://crystal-lang.org/
-
What languages are useful for contribution to the GNOME project.
Crystal is a nice language that's not only simple to read and write but performs very well too. And the documentation is amazing as well.
-
Jets: The Ruby Serverless Framework
Ruby is a super fun scripting language. I much prefer it to python when I need something with a little more "ooomph" than bash. It's just...nice...to write in. Ruby performance has come a long way in the last decade as well. There's libraries for pretty much everything.
My modern programming toolkit is basically golang + ruby + bash and I am never left wanting.
I do find Crystal (https://crystal-lang.org/) really interesting and am hoping it has its own "ruby on rails" moment that helps the language reach a tipping point in popularity. All the beauty of ruby with all of the speed of Go (and then some, it often compares favorably to languages like rust in benchmarks).
What are some alternatives?
purescript - A strongly-typed language that compiles to JavaScript
zig - General-purpose programming language and toolchain for maintaining robust, optimal, and reusable software.
rust-ordered-float
Nim - Nim is a statically typed compiled systems programming language. It combines successful concepts from mature languages like Python, Ada and Modula. Its design focuses on efficiency, expressiveness, and elegance (in that order of priority).
lang-team - Home of the Rust lang team
go - The Go programming language
idris - A Dependently Typed Functional Programming Language
Elixir - Elixir is a dynamic, functional language for building scalable and maintainable applications
rust - Empowering everyone to build reliable and efficient software.
mint-lang - :leaves: A refreshing programming language for the front-end web
genType - Auto generation of idiomatic bindings between Reason and JavaScript: either vanilla or typed with TypeScript/FlowType.
Odin - Odin Programming Language