AFAIK Gleam does not have GADTs, only regular ADTs
2 Likes
I see!
Still wondering what you could do in Cure that you couldn’t do in Gleam. Apparently I have my head wrapped around ADTs but not GADTs. Would Cure vs Gleam be a question of the complexity of the domain?
I haven’t looked at Cure or Gleam in any great detail but the most obvious difference to me is syntax - Cure has def ends which is much more like Elixir. It does also look like @mudasobwa is targeting Cure as a complementary tool to Elixir and Phoenix:
So for instance as per your example:
In specialist cases where Elixir might not be a good fit Elixir users might opt for Cure because its syntax is familiar/more in line with their taste. Those who like Rust/ML languages might opt for Gleam (IIRC Gleam’s syntax was inspired by Rust/ML languages).
Ultimately each language has to carve a space for itself and syntax is an important and deciding factor (as is general philosophy and USP). I wish both Cure and Gleam all the best - if they can bring more people to the BEAM, great!
One thing I would add which I have said elsewhere on the forum is that due to the advancement of LLMs I think it will be harder for the newer languages to gain traction, so if Cure really is designed to complement Elixir (rather than be a competitor to it) it could be a very smart move…
2 Likes
Is there any interesting story with how Cure handles effects?
I may be incorrect but dependently typed languages (of which Cure is one) allow a developer to far more tightly constrain the type checking done by the compiler. The canonical example is a Vector. If I type something as a Vector I have no way of constraining its size. Dependently typed allows me to create a type which is Vector of a specific size. It also allows me to specify types of functions (for example AddToVector) with the notation that the result will be a Vector (or whatever type) plus the added elements. The compiler can then try to see if there is any code which violates that constraint. I’m not as versed in CS as I’d like to be–I think there may be some reasons that it cannot be checked in certain cases but I may be remembering incorrectly.
I think the main concern about dependently typed is performance but I’m sure someone will correct me if I’ve gotten that point (or any of the others) wrong! 
3 Likes
I don’t think this is the case. From reading the documentation it seems that both have static type systems, but that’s where the similarities end. Gleam and Elixir have much more in common than Gleam and Cure do.
Compared to the stated features of Cure’s website Gleam offers very little in terms of static-analysis enforced correctness. If Cure’s static analysis functionality is a fighter jet then Gleam’s is a paper plane!
It will be interesting to see how the language develops. Both dependent types and SMT verification are active open areas of computer science research, and while useful and extremely powerful, how to make either of them approachable and productive in a language is an unsolved problem. Idris may be the most successful project there for dependant types, but even then it is a very challenging language to learn and write.
I couldn’t find any documentation on these features in Cure, and I wasn’t able to get any of the examples to compile and run, so I can’t say anything specific about their approach. I’m looking forward to seeing more as the language matures!
Dependant types are very slow to compile, however at runtime they can be used to produce significantly improved performance, as the compiler knows much more about the program. Unfortunately this benefit is likely not possible for Cure, as the BEAM doesn’t permit the programmer to disable runtime type checking. If it did Gleam could do that, making it substantially faster than Erlang or Elixir!
5 Likes
I have a hard time believing this to be true, unless you’re thinking about cases where users are writing suboptimal code with a ton of unnecessary guards and pattern matching.
Can you give a more concrete example where the compiler lacks, bonus point if you throw some BEAM assembly in there too! 
It’s not that the compiler is lacking at all, it’s just a property of the sort of virtual machine that the BEAM is. All operations on such a virtual machine will check the type tag of the values given to them and raise an error if the types are not appropriate for the operation. The cost of this checking is small, but since it applies to every single operation it ends up having a significant impact on performance. Systems that do not have these checks (e.g. C, OCaml, Chez Scheme with checks disabled) have greater performance in this area.
Erlang’s JIT compiler is really pretty good, and when it’s type analysis can infer that the data will always be of a specific type (such as there being guards at the level above) it will emit code that doesn’t do any runtime checks! This is a big part of why the JIT is so fast.
Understanding all the possible shapes the data can have at runtime is a hard requirement for omitting these runtime checks, and Erlang’s static type analysis is very limited, so unfortunately this optimisation cannot be applied often. Other BEAM languages such as Gleam and Purerl (and presumably Cure!) have total and perfect type analysis, so theoretically they could apply the optimisation to the entire program, but there is no way to do this on the BEAM.
2 Likes
I’m looking forward to seeing this being push upstream, I’m sure with the upcoming type system then there would be more reasons to improve the compiler in a way that it could take advantage of this information.
Elixir’s type system is a fantastic bit of engineering and very useful, but I am sceptical that it’d be able to provide information that the BEAM’s static analysis cannot. Elixir’s type system is gradual, so intentionally not total, while the BEAM’s static analysis is designed for this specific task.
The OTP team won’t ever accept anything other than total confidence in the type analysis, and we won’t ever have a “just trust me!” style API as found in Chez Scheme. It’ll always be based upon what can be inferred from the Erlang or the bytecode, and any extra information from 3rd party static analysis could not be used.
Do you mean syntax or how it works under the hood? Syntax-wise Cure appears to be a lot more like Elixir - in the same way Elixir was a lot like Ruby, and Elixir being different under the hood did not impede adoption of it from the Ruby community*, in fact given a very large number of Elixir’s earliest adopters were from Ruby does suggest my hypothesis, that syntax matters, may be correct.
I had a whole section on syntax in my What’s special about Ruby blog post. Syntax mattering may be more important to those who have an eye for aesthetics and feel (so those who tend to like languages like Ruby and Elixir).
*Just for clarity’s sake I don’t think people will leave Elixir for Cure, but rather may opt for it when there is a tangible specialised need for it.
1 Like
I mean the semantics of the language and the experience of working with it. Elixir and Gleam are rather conventional programming languages, while Cure’s feature set would make it very different.
It’s hard to say as Cure isn’t documented yet, but the stated features could make it a good deal more sophisticated than languages like Idris, and potentially even more challenging to understand and to write.
I agree syntax is important (I believe Gleam’s syntax was a key part of it’s success), but the challenge of learning to use dependant types and SMT-validation are dramatically greater than the complexities found in other programming languages, so in this specific case I think syntax is comparatively unimportant. To replicate the functionality of a trivial program in Elixir or JavaScript in a language with these features would be quite an accomplishment, and indicate the programmer has invested a great deal of time and effort into studying advanced type theory and its application.
1 Like
Similarly, Elixir from a Rubyists perspective was a paradigm shift, with Elixir being a functional language, introducing concepts like pattern matching, processes, message passing, etc. But it solved a particular problem - as it could be argued other languages did - but people still opted for Elixir despite it being so different.
If you’re saying Gleam and Cure are so different that they wouldn’t be in that position to begin with (where someone is having to decide between them to do something that Elixir might not be suited to) then it eliminates Gleam or Cure from the equation entirely depending on what they can or can’t do or what they are or are not suited to.
Ultimately, it would probably boil down to:
- What can Gleam do that Elixir can’t
- What can Cure do that Elixir can’t
- Out of the above, what can Gleam AND Cure do, and out of these which is the more compelling option depending on complexity/syntax/other things that are important to that particular user
From what you’re saying it seems that Cure and Gleam aren’t really designed to solve the same kind of problem or in the same kind of way, in which case it would make the decision easier.
Sorry, I’ve been unclear. I’m not saying just that it’s different in a way that Ruby’s OOP is different to Elixir and Gleam’s FP, it’s radically more challenging than anything found in any of those languages.
Dependant types and SMT validation are open areas of computer science research, especially their practical application in programming. The concepts that Elixir, Gleam, or Ruby each introduce were all well understood and in use 40-50 years ago, and they are trivial by comparison.
Note I’m not being critical of Elixir or Gleam or Ruby here. Being well understood and easy to use is a positive, not a negative.
1 Like
I don’t know enough about SMT validation to comment on how radically different Cure might be but if it’s as much of a paradigm shift as you say, and that they’re designed to be used in very different scenarios or purposes, then there probably won’t be a major cross-over or competition between them. Elixir users will continue to use Elixir until there is a need to use Cure for something it excels in or offers - and the same might be true for Gleam, Gleam users might also opt for Cure for those specialist use-cases.
I guess we’ll just have to wait for more info to see what Cure’s USP is in real world use.
Not yet. Technically, this is not the first priority because effects make it drastically harder to use SMT solvers, and Cure is supposed to be used to implement critical parts of the logic and then call it from other BEAM langs.
My bad. I posted an announce too early because after a months deeply in, I was under the wrong impression that everything is evident and clean 
That’s definitely not the killer feature. Despite I have put some effort to optimization, Cure does not aim to be faster. It aims to be proved to be error-free.
Disclaimer. I got a COVID and I am off the grid until next week or so. Thanks everyone for understanding. I see there is an interest in what I am doing and therefore I’ll start with a proper timeline, and feature plan. Until now I was in a rush to make it work from Cure code through type checker, code gen and runtime, which is confusing for newcomers.
6 Likes
Wishing you a speedy recovery!
3 Likes
Could be nice to have, but you definately don’t owe us (or anybody else) anything.
1 Like
That’s the impression that I got.
I might be in the minority, but I love the idea of having layers of the application that are pure functions only.
1 Like
Cure is providing such a layer, yes. Exactly.
When it comes to unpureness, the implementation becomes either pure unmaintainable beauty (see Brady’s implementation of printf for Idris, the mindblowing piece of art, which converted me to the Dependent Types Coming Witness,) or a bunch of compromises, sacrificing the whole idea of pure functions.
Once we are on BEAM already, I decided not to try to lift three times my weight, but rather do what I can do without hacks and delegate to other BEAM langs to handle effects.
