purescript
Idris2
purescript | Idris2 | |
---|---|---|
54 | 40 | |
8,716 | 2,676 | |
0.2% | 0.8% | |
3.9 | 8.9 | |
11 days ago | 2 days ago | |
Haskell | Idris | |
BSD 3-clause "New" or "Revised" License | GNU General Public License v3.0 or later |
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.
purescript
-
An Ode to TypeScript Enums
When I see this it makes me want to run for ReasonML/ReScript/Elm/PureScript.
Sum types (without payloads on the instances they are effectively enums) should not require a evening filling ceremonial dance event to define.
https://reasonml.github.io/
https://rescript-lang.org/
https://elm-lang.org/
https://www.purescript.org/
(any I forgot?)
It's nice that TS is a strict super set of JS... But that's about the only reason TS is nice. Apart from that the "being a strict super set" hampers TS is a million and one ways.
To my JS is too broken to fix with a strict super set.
-
How I host Elm web applications with GitHub Pages
A web application makes use of these same ingredients, i.e. HTML, CSS, and JavaScript, but it uses significantly more JavaScript. As the JavaScript powering your web application grows in size it can bring with it a variety of problems that a few languages, like TypeScript, ReScript, PureScript, and Elm, have attempted to solve. Each of the aforementioned compile to JavaScript languages have their pros and cons but it is beyond the scope of this article to get into those details. Suffice it to say, my preference is Elm. It is also not the goal of this article to convince you to use Elm but only to show you how Elm fits into the flow of creating a web application and hosting it on GitHub Pages. So let's continue by adding Elm to our project.
- Learning Elm by porting a medium-sized web front end from React (2019)
- Ask HN: Interest in a Rust-Inspired Language Compiling to JavaScript?
-
Building React Components Using Unions in TypeScript
Naturally I’d recommend using a better language such as ReScript or Elm or PureScript or F#‘s Fable + Elmish, but “React” is the king right now and people perceive TypeScript as “less risky” for jobs/hiring, so here we are.
-
Is there a better way to do read-only types
Unless you want to switch to https://www.purescript.org/.
-
Why I'm Leaving Elm
PureScript[1][2] seems pretty alive these days. From my relatively small, self-contained experiments, it's a lot more flexible and expressive than Elm at the expense of (maybe?) being a bit harder to learn up-front.
[1]: https://www.purescript.org/
[2]:https://github.com/purescript/purescript
- (strongly typed) functional language compilers running in browser
-
purescript VS purs-eval - a user suggested alternative
2 projects | 2 Mar 2023
- Por que Elm é uma linguagem tão deliciosa?
Idris2
-
De Bruijn notation, and why it's useful
Idris[1] and most of the dependent typed languages that I've looked at use de Bruijn numbers. (As does my own[2].)
The Idris implementation also has a list of names in scope as an argument to the type of a Term, which makes the compiler (also Idris) check if you're making a mistake with your de Bruijn indices. (I did not do this in mine, but I should have.)
[1]: https://github.com/idris-lang/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
-
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
What are some alternatives?
elm-reactor
genType - Auto generation of idiomatic bindings between Reason and JavaScript: either vanilla or typed with TypeScript/FlowType.
rescript - ReScript is a robustly typed language that compiles to efficient and human-readable JavaScript.
lang-team - Home of the Rust lang team
liquidhaskell - Liquid Types For Haskell
smalltt - Demo for high-performance type theory elaboration