Candy – a minimalistic functional programming language | Hacker News Reader

Candy – a minimalistic functional programming language

github.com

79 pointsmicroflash63 comments

> Dividing by a string fails during compilation with a type error, while dividing by zero only fails during runtime. In the mathematical sense, there's no fundamental difference between these cases – division is only defined for divisors that are non-zero numbers.

It seems there is a fundamental difference: zero-ness is a value property while number-ness is a type property. That makes the latter trivial to check at compile time.

> That's why we eliminate the border between compile-time and runtime errors – all errors are runtime errors.

That seems like a step back from having an editor type-check your code.

> By crafting high-quality tooling with dynamic analyses such as fuzzing, we try to still be able to show most errors while you're editing the code.

But fuzzing takes more resources than typechecking. I'd prefer to always do the latter, and make the former optional , as Haskell does with QuickCheck.

> It seems there is a fundamental difference: zero-ness is a value property while number-ness is a type property. That makes the latter trivial to check at compile time.

That's because you have defined division to have two number inputs. Nothing stops you from defining it having a number and a non-zero number as an input. And a non-zero number can only be constructed with an enforced run-time check. For an example look into NonEmpty in haskell. A list type which always contains at least one element.

Look at it this way. Underneath everything is bits anyway. Everything we have build on top is just "types" in a certain sense.

> It seems there is a fundamental difference: zero-ness is a value property while number-ness is a type property

The distinction is up to the programming language designer to define. You absolutely could define types such that divide-by-zero is caught as a type error. You'd need a Zero type and a NonZeroNumber type, and have Number be the superset of them. Then define division over Number / NonZeroNumber.

This breaks down because it's not easy to statically reason about when a variable is a NonZeroNumber. For example, what is the type signature for subtraction of two NonZeroNumbers? You can't guarantee that it isn't zero, so it has to be a Number. Thus, you can't divide by the difference. You could use a more powerful type system to reason about these kinds of constraints, but then type checking quickly becomes undecidable (or at least very, very expensive).

> For example, what is the type signature for subtraction of two NonZeroNumbers? You can't guarantee that it isn't zero, so it has to be a Number.

You can encode this failure as well, so at least the possibility becomes explicit:

    NonZero -> NonZero -> Either NonZero Number

Oleg also showed you can make an even safer statically checked version with pretty standard type theory and modules:

https://okmij.org/ftp/Computation/lightweight-guarantees/lig...

    a = b - c

    if a != 0 then x = y / a

Here you can infer that the type of 'a' inside the 'then' is a NonZeroNumber. "All" you need is for the type checker to be able to recognize when a conditional acts as a guard against a subset of the possible types.

But if we're dividing by (a-1) then recognizing that it's safe may require a type NonOneNumber. And in other cases perhaps NonFortyTwoNumber. Where does that end?

Only in as much as it would require the type checker to be able to express and operate on expressions constraining or combining types, not name every one. E.g. being able to recognise that in this:

   if a < 2 then exit

.. afterward, "a" has a named numeric type fully covered by its previous type combined with the extra constraints of the check if that allows picking a more constrained type, and its real type is further constrained to the subset a>=2, and be able to reconcile that this means 'a' can't be 1.

In practice, yes, you can absolutely get into situations where this will mean you end up writing extra checks to prove to the compiler that a value can only be within the required subset if the type checker couldn't figure it out. How often will depend on how advanced your type checker is.

Why only go that far? You can have types for One, Two, Three … Inf and then define division of type Four by type Two as type Two and so on. This would eliminate the need to actually run your program since your type checker would be Turing complete and all code would run in Zero time.

That's completely feasible and there are languages that do this. It doesn't really eliminate the need to run your program unless the inputs to your program are also completely restricted types like One, Two, Three. In which case yeah, you don't need to run it and the type system can just tell you the answer.

I believe you can do that sort of thing in loads of type systems, e.g. Typescript, but there are languages that intentionally support it. I use a niche DSL that has fancy types like this called Sail. https://github.com/rems-project/sail

In my experience the downsides of these fancy "first class type systems" are

1. More incomprehensible error messages.

2. The type checker moves from a deterministic process that either succeeds or fails in an understandable way, to SMT solvers which can just say "yep it's ok" or "nope, couldn't prove it", semi-randomly, and there's little you can do about it.

Still my experience of Sail is that it's very comfortable to go a little bit further into SMT land, and my experience of Dafny is that it's very unpleasant to go full formal-verification at the moment.

I've done a fair bit of hardware formal verification too and that's a different story - very easy and very powerful. I'm hoping one day that software formal verification is like that.

> You can have types for One, Two, Three … Inf and then define division of type Four by type Two as type Two and so on

That's not far from TypeScripts type system

That's essentially what dependent typed languages do. But the stuff that happens at type checking level has to be known to terminate, so it isn't Turing complete. Without this restriction, it is possible to prove false things to the compiler by writing code that never returns.

But what if we use predicate-based typing? Then your "type" will be something like `(x) ↦ (0 < x < ∞)`, holding true only if the value matches it. Then, given the type function is pure, the hypothetical compiler may somehow optimize them out most of the production code that can be statically analyzed...

> we eliminate the border between compile-time and runtime errors – all errors are runtime errors.

> we try to still be able to show most errors while you're editing the code

This is not eliminating a border. It is adding a border strip between edit and run - covering all of compile.

And "all errors are runtime errors" tasks the compiler with compling erroneous code just to serve runtime detection.

> Fuzzing instead of traditional types. In Candy, functions have to specify their needs exactly. As you type, the tooling automatically tests your code with many inputs to see if one breaks the code

This is a neat idea and the screenshots make it look fun. There are a few features that once you've gotten used to, become hard to live without (syntax highlighting, autocomplete, unit tests, etc). I could see how this real-time fuzzing approach might be one of those. Would be fun to try.

I don't see how this is different from any other dynamically- and strongly- typed programming language with some kind of "contract" framework, like Clojure or Python.

Fewer types:

  Values are at the center of your computations. Only a handful of predefined types of values exist:

  3                   # int
  "Candy"             # text
  Green               # symbol (uppercase)
  (Foo, Bar)          # list
  [Name: "Candy"]     # struct
  { it -> add it 2 }  # function

Not having a Hash/Dict type is very oldschool lisp-y.

I assume a struct is a Hash/Dict type. Since you have no type checking all fields can be considered dynamic.

Exactly, structs are also used as maps/dictionaries, and the current implementation of them in our VM is as hash maps. (We have optimizations planned for this.) You'd create a struct with tags (symbols) as keys to create a typical struct/class, and can use arbitrary keys if you want to use it as a more general map:

  # A struct with two tags as keys mapping to functions
  httpServerStruct = [GetNextRequest: { … }, Close: { … }]
  
  # A map with text keys
  capitalCitiesMap = ["Germany": "Berlin", "France": "Paris"]

Even ancient Lisp was not without hash/dict processing. It was disguised in the interning of symbols, and symbol property lists.

If structs are just tables by another name, this sounds a lot like Lua to me. Not that there's anything wrong with Candy here, but I don't know that it's much of a departure from what we already have.

The real-time, nicely designed view of it as shown in the screenshots looks interesting.

What contract framework would you recommend in Python?

I've been dissatisfied with all of them actually!

But both Deal (https://pypi.org/project/deal/) and icontract (https://pypi.org/project/icontract/) have merit.

I can't remember where I saw it, but the author of deal seemed a bit annoyed at the existence of icontract, maybe on a mailing list.

I've played around with CrossHair (https://pypi.org/project/crosshair-tool/) as well a bit, and that supports both deal and icontract.

icontract also seems to integrate with hypothesis (https://pypi.org/project/hypothesis/) , which deal does not do explicitly.

deal actually has a far better integration with hypothesis as its testing strategies are built on that library! https://deal.readthedocs.io/details/tests.html#mixing-with-h...

Thanks a lot!

> I've been dissatisfied with all of them actually!

What are some of your dissatisfaction points? Do you know of better alternatives in other languages ?

In almost all (strongly typed) languages, there is still a need for runtime checks like divide by zero and array bounds checks. Certainly languages like Rust & Haskell bring a high level of static analysis and that is good when you are relying on the tool for memory safety.

Personally I prefer gradual type systems that need less up front wrestling so that the coding process is more productive, more time can be spent on tuning the design rather than “finally I made it work” acceptance of compiler driven design. Such languages such as Python, Raku use GC for safety so not perfect for embedded or OS type tasks but easier on the brain.

I mentioned Raku since it has extensive runtime type support which allows code like:

    subset Zero of Int where * == 0;
    subset NonZero of Int where * != 0;

    multi infix:<div>(Int \a, Zero \b) {warn “you dolt”; Inf}
    multi infix:<div>(Int \a, NonZero \b) {a div b}

So Larry Wall chose to leverage a runtime typesystem to make it easier to write and maintain code rather than go down the straitjacket route.

> Personally I prefer gradual type systems that need less up front wrestling so that the coding process is more productive, more time can be spent on tuning the design rather than “finally I made it work” acceptance of compiler driven design.

If your style is to hack hack hack until it’s right, yeah, types are challenging. If your style is to think first about types, you can also create guardrails in your code that naturally create the correct thing.

Static vs Dynamic vs Gradual… it’s really more a question of “how does my brain like to get to a solution and keep it functioning” and I find that fascinating.

> it’s really more a question of “how does my brain like to get to a solution and keep it functioning” and I find that fascinating

Sure, but this is largely a matter of training and experience. Plenty of fans of dynamically typed languages just haven't learnt how to make effective use of decent static type systems.

Static type systems are premature optimization, and come with all of its problems.

So a more fluid solution is a great thing, if done right. TypeScript comes to mind, although it has other problems, in particular mutable data structures by default.

Why do you say that static type systems are a "premature optimization"? On its face, that seems like a (very spicy) opinion that's been stated as fact.

It is a fact, that is why I state it as one. You are basically trying to write a correctness proof before you actually have a good idea of what it is you are trying to build. I've done this plenty of times myself, and it is a good way to waste time and tell yourself you are productive. Yes, I am also looking at all the "let's rewrite stuff in Rust" projects.

Especially problematic is that the type system doesn't necessarily reflect the correctness you care about, but just some properties the language cares especially about. You are spending your time trying to shoehorn your solution into somebody else's idea of correctness, who doesn't really know anything about your program at hand.

That's why I like TypeScript, its type system is expressive enough for many simple correctness checks I actually care about, while at the same time not getting (too much, and with the above caveats) in the way of how I think about what I build.

It is especially clear to me that static type systems are dinosaurs of the past. The future is on-the-fly checking of arbitrary logical properties of your program, which can always contain what static type systems used to be for as a subset.

> You are basically trying to write a correctness proof before you actually have a good idea of what it is you are trying to build. I've done this plenty of times myself

This is where I think the commenter towards the top of this thread has it right:

> If your style is to hack hack hack until it’s right, yeah, types are challenging. If your style is to think first about types, you can also create guardrails in your code that naturally create the correct thing.

Your experience with static typing is that of someone whose personal style is to write code as an exploratory process while you're trying to figure out what to build, and from the sound of it you were trying to do that in something like Java before you switched to TypeScript. And I completely agree—that style is a terrible match for a Java-like type system.

But there are type systems besides TypeScript that are much more flexible than the kind that you're thinking of, and there are styles of software engineering that don't involve extensive prototyping as part of the development process. Those styles—typically slower and data-centric—combine really well with strong and flexible type systems (even something like modern Java with sealed interface goes a long way), and you're doing yourself a disservice by assuming that everyone who uses those styles is just wasting a lot of time.

I've been programming with Standard ML pretty much since 1995, so I know a thing or two about powerful type systems. Of course there are different kinds of software and different kinds of styles to write this software. Some software needs a correctness proof, other software doesn't, because if it seems to work, that is good enough. If your type system aligns well with the kind of correctness you need for your software, sure, that's good, go for it. A type system is better than nothing at all (that's why I much prefer TypeScript over JavaScript), but it is only an approximation of what you really want (your program fulfils its purpose). If that approximation is good enough for you and your problem domain, fine. Just be aware that the time you spend thinking about how to best fit of what you want to do into your type system, is probably not the best way to work on what to build and how to build it, although it might feel to you that way.

> if it seems to work, that is good enough

I think that's where many people would disagree with you.

Also static types are not only about correctness. They also greatly help with understanding, documentation and navigation.

The two biggest third party codebases I've contributed to are VSCode and Gitlab. VSCode was about 10x easier than Gitlab simply because I spent so much time in Gitlab just trying to find the code that a function called, or the code that called a function. (I think Ruby also encourages ungreppable code styles which makes this even worse.)

In VSCode it was pretty much just one click. (Occasionally more because of abstract interfaces, but even then way way nicer.)

Anyway yeah obviously if you don't really care about your code working or being readable then you are going to feel like static types are a waste of your time. That's kind of like saying that showering is a waste of time because you don't need to be clean.

> I think that's where many people would disagree with you.

And they would be wrong, because for some classes of software, if it seems to work, that is actually the definition of working and fulfilling its purpose. Because there is no clear definition of what "correct" would mean.

But that's not the point. Read my comments to see where I am coming from.

I guess you are talking about art projects? Yeah I don't think you can base a generic argument on a tiny niche programming domain.

"some" is an existential quantifier. To prove an existential statement, you only need a single example. So of course I can base an argument on that, especially if it just illustrates the range of different purposes of software.

This is a debate, not a mathematical proof.

> the time you spend thinking about how to best fit of what you want to do into your type system, is probably not the best way to work on what to build and how to build it

I think this is mistaken, but is getting close to the heart of the matter.

The following describe identical sets:

• Developers who know how to make effective use of a decent static type system

• Developers who are able to follow a development methodology that deeply incorporates a language's static type system, such that the static type system becomes a useful tool integral to the development process rather than a hindrance

Developers who view static type systems as just a nuisance - a malicious demon that must be propitiated at wasted expense - very often just lack the skills to make effective use of the type system. They mistakenly assume that it must not be possible at all, and that the folks speaking to the benefits of static type systems must just be talking nonsense.

Many developers start out seeing static type systems as a hindrance, but gradually learn more about static typing and eventually come around to its advantages. I'm one such. I'm sure many of the really hardcore static typing folks (the wizards of Haskell and Scala) had the same experience.

Anecdotally, it seems to me that relatively few developers tell the story in reverse, starting out with a deep competence in programming with static type systems and gradually coming around to dynamic typing. It sounds like you may have had exactly this experience, but I think this is uncommon. (Again, this is of course just anecdotal.)

A similar thing goes for other software development skills such as version control. Plenty of developers start out seeing version control as frustratingly finicky and complex, but gradually build up mastery of their version control system and end up treating it as an integral part of their development process. Approximately nobody does this in reverse, abandoning a system like git for a free-form approach.

All that said, there are times when heavyweight tools like static type systems and version control just aren't necessary. The applicability of their benefits and drawbacks do of course depend on context.

> Some software needs a correctness proof, other software doesn't, because if it seems to work, that is good enough.

I don't think this is meaningful. There is no seems to work, a bug either exists or it doesn't.

> A type system is better than nothing at all (that's why I much prefer TypeScript over JavaScript)

Pedantic nitpick: this implies JavaScript is an untyped language, which is not the case, it's a dynamically typed language. There are very few languages that lack a type system of any kind, pretty much just assembly and Forth.

> it is only an approximation of what you really want (your program fulfils its purpose)

Right, but no one is suggesting a type system can entirely replace a test suite. Static type systems offer only a fraction of the assurances of full correctness proofs, but are incomparably easier to use.

> Especially problematic is that the type system doesn't necessarily reflect the correctness you care about, but just some properties the language cares especially about.

You're neglecting that these guardrails guide you towards solutions that can be naturally expressed and checked by the language. That's a feature, not a bug.

> The future is on-the-fly checking of arbitrary logical properties of your program, which can always contain what static type systems used to be for as a subset.

Yeah, except for logical consistency or soundness, but who cares about that?

No, I don't neglect that. These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution. There is a lot of religion and faith involved here.

I care a lot for logical consistency and soundness, probably more than anyone else you know. But it is wrong to think that static type systems are the best way towards this. Logic is the best way towards this, and static type systems are just one way of implementing logic, and not the best one.

Especially in programming, what static type systems were really good at, was automating some correctness checks. I believe in a future where automation gets so good that static type systems become a hindrance, and where their benefit vanishes when weighed up against your freedom to express things as they really are.

> These guardrails are guiding you towards something, but it is very optimistic to assume that they guide you towards the best solution.

"Best solution" is a fantasy. Any solution must be expressed in a language with concrete semantics, but there is no best language for all possible problems. This was the lesson of Kolmogorov complexity.

Therefore, we will always necessarily be using a suboptimal language, and we should let go of any wish for ill-defined optimality. We should instead use a language that guides towards engineering good solutions to problems with desirable properties. Sometimes that might mean strict control over resources (as with Rust), sometimes that isn't necessary (so OCaml,F#, etc. would do).

An empirical fact of engineering is that most mistakes people make are trivial, eg. typos, one off errors, forgetfulness to change code in all relevant places during refactoring, etc. Good abstractions enforced by static types solve all of these problems, allowing you to focus on the core problem without being bothered that you might have missed some silly details. Yes the compiler bothers you to correct these details, but this is typically simple mechanistic work that nevertheless can't be automated by any other language without sacrificing other desirable properties.

I'm not going to argue that any static type system is better than no static types, because it's easy to invent a bad type system. We've had pretty damn good type systems since the 70s though, they just didn't see much use until recently.

"Best solution" is a proxy here for the software you really want. That's what you need to go for; if you don't, I don't really want to use your software, although I might have to, because there is nothing else.

Again, a good general type system that catches simple mistakes is better than nothing, I agree with you here! But Rust for example, isn't that. It is quite invasive in terms of how you have to think about your program, and if your way of thinking or your particular problem aligns with Rust's approach, great. Most of the time, it will not. So if you choose for example Tauri over Electron, most of the time, that will be the wrong choice.

Anyway, static type systems are a crutch. They've been useful in the past, mainly because they allow to automate partial correctness. In the future, we will have something better (I am not saying we will have something "optimal", although it might feel that way compared to the current state of things).

Yes, Rust is invasive because it guarantees certain properties that are otherwise very difficult to guarantee, and by all reports, once you build the requisite mental model it becomes much more straightforward, which is typical of static typing and programming in general.

Re: static typing being a crutch, I disagree, and I think more, better typing is in our future, not less. We'll see how it goes.

But let's be clear what we are talking about here, so we can see who wins the bet:

I am betting against static typing, but on general logic. So I am betting against a static type system being the future, instead I think a general logic will be the future, not only of programming, but of all engineering.

The misconception that all "early optimization" is premature optimization is a dangerous one.

I'll agree with you that starting with static type systems is an early optimization. But if it's premature or not is clearly context dependent. And it is often "right on time" optimization. Just as are many things engineers like to deride as "premature optimization".

It's not premature if it's known to be needed and the cost of doing it later greatly outweighs doing it now.

And plenty of them wouldn't want to learn it, so I think OP's observation still holds.

I've been getting a lot of mileage out of Julia recently, and would counter that plenty of fans of statically typed languages just haven't learned to use an effectively-typed dynamic language.

It's great, give it a shot sometime.

Here, lemme help those of you who would rather use your reflexes than your frontal cortex https://docs.julialang.org/en/v1/manual/types/

It's possible to get the advantages of a dynamic runtime and the advantages of a powerful type system, Julia is proof of that.

I think there's a line or maybe some Venn Diagram meme about hack back hackers and "I'll refactor this later".

Not trying to start anything with either type. We're all guilty of these platitudes and well intentioned lies.

I like Raku (it fits my brain as I was programming a lot of Perl in the 90s) and I like these features. You want to be able to do this. A lot of this you can easily make static though (so you have both) (maybe that happens under the hood?).

Neat! The idea that 'types are just constraints on values that happen to be checked at compile-time' is something I've been thinking about for a long time. I've been thinking about building a Scheme-like language on the same principle.

  (define (my-function some-number) (assert (is-int some-number)) (assert (is-nonzero some-number)) (...body of function goes here))

That way you can start with a dynamically typed language and slowly add type information (and any other constraint you want) without having to modify the syntax. A Sufficiently Advanced Compiler may be able to detect problems that e.g. `javac` wouldn't. But I'm probably repeating what the Candy devs already said in their readme.

The thing holding me back, aside from general indecisiveness and getting stuck in bootstrapping loops (I immediately get annoyeed with existing build tools and want to write my own...in my language that doesn't exist yet) is that I wonder if I should learn about dependent types, first, in case it totally changes my approach. I've had a PDF of The Little Typer open to some page in chapter 2 for months, now.

Another concept I want to embed is that there are no fundamental structural types. e.g. anything that acts like a list is a list. What you really want to know is the 'color'[1] of values, i.e. 'what does this value MEAN'. Because you can represent anything as a list, and especially in dynamically-typed languages, it's not always obvious if you're supposed to e.g. interporet a list as a list, or as something else, represented by the list. "You must beware of shadows", as they say. Maybe what I want is 'dynamic structural types but static coloring'.

[1] term borrowed from the JavaScript world, often referred to as the 'function coloring' problem, though it's not really about the function so much as the values they take and return. "Is this promise you just passed me standing for itself, or did you want me to calculate something based on the promise's result value?"

not exactly what you describe but it may be worth looking at (gradually) typed racket in this context: https://docs.racket-lang.org/ts-guide/. the contract system might also be of interest: https://docs.racket-lang.org/reference/contracts.html

It might be fun to besides doing fuzzing, use other software correctness / formal methods tools such as abstract interpretation or type systems to report run-time errors. I mean, fuzzing will not detect all runtime errors, so the formal methods crowd might suggest to just throw all your tools in the toolbox to maximize run-time error elimination.

Delegate everything to fuzzing is fun though (fitting for the name "candy" and the minimalistic premise).

You might be interested in https://dafny.org/

compare https://github.com/webyrd/Barliman

I have take a weakness for languages like Candy. A word of warning for those eager to dive in like myself. Candy seems to require a nightly build of Rust from 2024-02-22 (that's two days ago). After building, it gave me a 157MB binary that either seems to panic or print nothing when I run the examples. I assume the only way to really use it right now is from VSCode, and trying to run the CLI tool (as I did) just doesn't work. I'd love to give it a go, but I might have to wait a few more weeks.

We're using some unstable features (hence nightly), and I just updated our Rust version on Thursday (https://github.com/candy-lang/candy/pull/948) because the previous one (nightly-2023-07-21) was too old for a dependency. So we're not usually using this recent Rust versions.

Thanks for letting us know about the binary size! We previously enabled debug info in release builds to use flamegraphs, but actually don't need it for most builds. I just disabled it (https://github.com/candy-lang/candy/pull/950), and the binary size went down from 177.4 MB to 14.2 MB for me!

The CLI should work, or at least we're using it regularly when working on Candy. Can you please share your OS and the command and output, maybe in a GitHub issue? We definitely need to improve our documentation and the CLI's error handling. Does running `cargo run --release -- run ./packages/Examples/helloWorld.candy` from the repository root work for you?

The VS Code extension also uses the CLI internally since that exposes a language server, so it basically runs `cargo run --release -- lsp`. But we also have to improve the stability here.

Thanks for the reply! I think I've figured out why I couldn't get any of the examples to run. I was using the debug build rather than the release build. Take sqrt.candy for example, it takes 26 seconds to compile (25s) and execute (1s) with the debug build, and only 1 second to compile and execute on the release build. This is on a Ryzen 7700X, one of the fastest single threaded CPUs.

Similarly, average.candy takes 24s to compile the 10 line program that only depends on Core and averages three numbers (1, 2, and 3). clock.candy takes 39s to compile and then panic. echo.candy takes 23 seconds before prompting and echoing the input. file.candy takes 26s before panicking, and so on. I never waited long enough to see any of the programs work. Thanks for pointing me at needing to use --release.

  cargo run -- run ./packages/Examples/sqrt.candy  26.28s user 0.11s system 100% cpu 26.392 total
  cargo run --release -- run ./packages/Examples/sqrt.candy  0.97s user 0.08s system 100% cpu 1.052 total

Fuzz testing seems surprisingly powerful as part of an IDE and doesn't require any new annotation but seems to waste a ton of resources... I wonder if someone developed an algorithm for most efficiently breaking your assertions, perhaps even with a pre-fitted probabilistic heuristic guiding the search.

> That's why we eliminate the border between compile-time and runtime errors – all errors are runtime errors.

That's the opposite of what I want. I want as many errors as possible to be compile-time errors, so that I know I'll catch them all during development instead of as bugs in production.

Wonderful new stuff.

I heard it suggested recently that it would be interesting to build a static analysis system around proving that code was wrong (as opposed to proving that certain classes of bugs were missing). Fuzzing seems like one reasonable approach. Love the editor integration too.

Reply on news.ycombinator.com