24 ms·

Candy – a minimalistic functional programming language

79 points by microflash 3y ago

tromp 3y ago
> 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.
- idle_zealot 3y ago
  > 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.
  - librasteve 3y ago
    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.
    - timhh 3y ago
      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 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.
    - zokier 3y ago
      > 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
    - dunham 3y ago
      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.
  - obastani 3y ago
    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).
    - naasking 3y ago
      > 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/lightweight-static-capabilities.pdf https://okmij.org/ftp/Computation/lightweight-guarantees/lig...
    - vidarh 3y ago
      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.
      - tromp 3y ago
        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?
        vidarh 3y ago
        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.
  - pona-a 3y ago
    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...
- ildjarn 3y ago
  [dead]
- rowanG077 3y ago
  > 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.
chrisjj 3y ago
> 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.
runeblaze 3y ago
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).
- 082349872349872 3y ago
  compare https://github.com/webyrd/Barliman https://github.com/webyrd/Barliman
- IshKebab 3y ago
  You might be interested in https://dafny.org/ https://dafny.org/
breck 3y ago
> 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.
- nerdponx 3y ago
  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.
  - sdeframond 3y ago
    What contract framework would you recommend in Python?
    - nerdponx 3y ago
      I've been dissatisfied with all of them actually! But both Deal (https://pypi.org/project/deal/ https://pypi.org/project/deal/) and icontract (https://pypi.org/project/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/ 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/ https://pypi.org/project/hypothesis/) , which deal does not do explicitly.
      - sdeframond 3y ago
        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 ?
librasteve 3y ago
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.
- apgwoz 3y ago
  > 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.
  - deprecative 3y ago
    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.
  - MaxBarraclough 3y ago
    > 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.
TOGoS 3y ago
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?"
- disconcision 3y ago
  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/ https://docs.racket-lang.org/ts-guide/. the contract system might also be of interest: https://docs.racket-lang.org/reference/contracts.html https://docs.racket-lang.org/reference/contracts.html
deleted 3y ago
[deleted]
nmca 3y ago
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.
quag 3y ago
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.
- JonasWanke 3y ago
  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 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 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.
  - quag 3y ago
    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
josephcsible 3y ago
> 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.
pona-a 3y ago
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.

79 points by microflash 3y ago

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

idle_zealot 3y ago
> 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.
- librasteve 3y ago
  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.
  - timhh 3y ago
    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 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.
  - zokier 3y ago
    > 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
  - dunham 3y ago
    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.
- obastani 3y ago
  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).
  - naasking 3y ago
    > 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/lightweight-static-capabilities.pdf https://okmij.org/ftp/Computation/lightweight-guarantees/lig...
  - vidarh 3y ago
    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.
    - tromp 3y ago
      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?
      - vidarh 3y ago
        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.
- pona-a 3y ago
  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...
ildjarn 3y ago
[dead]
rowanG077 3y ago
> 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.

chrisjj 3y ago

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

runeblaze 3y ago

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

082349872349872 3y ago
compare https://github.com/webyrd/Barliman https://github.com/webyrd/Barliman
IshKebab 3y ago
You might be interested in https://dafny.org/ https://dafny.org/

breck 3y ago

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

nerdponx 3y ago
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.
- sdeframond 3y ago
  What contract framework would you recommend in Python?
  - nerdponx 3y ago
    I've been dissatisfied with all of them actually! But both Deal (https://pypi.org/project/deal/ https://pypi.org/project/deal/) and icontract (https://pypi.org/project/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/ 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/ https://pypi.org/project/hypothesis/) , which deal does not do explicitly.
    - sdeframond 3y ago
      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 ?

librasteve 3y ago

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.

apgwoz 3y ago
> 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.
- deprecative 3y ago
  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.
- MaxBarraclough 3y ago
  > 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.

TOGoS 3y ago

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?"

disconcision 3y ago
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/ https://docs.racket-lang.org/ts-guide/. the contract system might also be of interest: https://docs.racket-lang.org/reference/contracts.html https://docs.racket-lang.org/reference/contracts.html

deleted 3y ago

[deleted]

nmca 3y ago

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.

quag 3y ago

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.

JonasWanke 3y ago
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 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 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.
- quag 3y ago
  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

josephcsible 3y ago

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

pona-a 3y ago

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.