IdrisExtSTGCodegen VS Idris2

In practice we will probably have an STG backend for Idris2 before a dependent Haskell, then at least you could link together Haskell and Idris code

I write an Idris2 backend which compiles to STG, yesterday we achieved to run the HelloWorld using functions from GHC.Base :) https://github.com/andorp/IdrisExtSTGCodegen/commit/0150510a7d6160806a85d799768d39f9acc65d30#diff-a15cf9e0e0625f8260bb7b91a4f4ca8e4f4558acf37d4cc834acd2e8a4cdf89aR6

There is a WIP Idris2 to Ext-STG compiler: https://github.com/andorp/IdrisExtSTGCodegen

Ah, the repo also has the slides of the talk, which are a nice first step to video-less content.

| The Idris language versions have always supported easy and modular code generation. I am working on the Idris-ExtSTG backend closely collaborating with Csaba. The progress can be followed here: https://github.com/andorp/IdrisExtSTGCodegen . I am going to give a talk about my experiences at BobKonf 2021: https://bobkonf.de/2021/penzes.html

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

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...

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.

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/

Idris2 has a great syntax for this, see e.g. node018:

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.

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

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