[HN Gopher] Candy - a minimalistic functional programming language
___________________________________________________________________
Candy - a minimalistic functional programming language
Author : microflash
Score : 29 points
Date : 2024-02-24 17:17 UTC (5 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| tromp wrote:
| > 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 wrote:
| > 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 wrote:
| 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 wrote:
| 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.
| zokier wrote:
| > 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
| chrisjj wrote:
| > 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 wrote:
| 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 wrote:
| compare https://github.com/webyrd/Barliman
| IshKebab wrote:
| You might be interested in https://dafny.org/
| breck wrote:
| > 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 wrote:
| 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 wrote:
| What contract framework would you recommend in Python?
| breck wrote:
| The real-time, nicely designed view of it as shown in the
| screenshots looks interesting.
| librasteve wrote:
| 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 wrote:
| > 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 wrote:
| 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 wrote:
| > 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.
___________________________________________________________________
(page generated 2024-02-24 23:00 UTC)