5 ms·

It's currently used as a back-end for the Idris language. (Which is primarily a research language, admittedly.) It's a fairly popular target for languages to

by retrac 3y ago

It's currently used as a back-end for the Idris language. (Which is primarily a research language, admittedly.) It's a fairly popular target for languages to compile to, for similar reasons that C is -- small, well-defined, minimal, many implementations, runs just about everywhere. Very nice compilation target for functional languages in particular, as call/cc can, with reasonable efficiency, implement just about any kind of control flow/evaluation/threading model that you can think of. Also, used as a scripting language in the GIMP.

tmalsburg2 3y ago
C is neither minimal nor well-defined, as has been discussed extensively. Random blog post illustrating only some of the issues is here [1]. Just google “undefined behavior c” for a lot more. There are also a bunch of famous rants by Linus Torvalds on his topic. [1] https://blog.regehr.org/archives/213 https://blog.regehr.org/archives/213
- PennRobotics 3y ago
  can we all agree that the undefined behavior is pretty well identified and documented? Plus, if you understand the entire language and then limit your imagination, C can be quite simple!
  - mrguyorama 3y ago
    It's so simple to avoid undefined behavior, just never add two numbers, or dereference a pointer that you can't statically guarantee the value of.
    - spookie 3y ago
      Yes, it's a simple language. That's why there are no safe guards around INT_MAX + 1, or variants of that.
    - fluoridation 3y ago
      You can add two numbers. If the operands are signed you just need to check the operands before the addition to make sure you won't cause an overflow.
      - deleted 3y ago
        [deleted]
      - johncowan 3y ago
        Which of course cannot be done portably except by drastic restrictions like "never add a number greater than MAXINT / 2 and never multiply a number greater than sqrt(MAXINT)".
        mananaysiempre 3y ago
        Soon™ we will have ckd_add etc. in the standard for this sort of thing, after several decades finally exposing functionality that any non-exotic CPU provides. Except RISC-V, because RISC-V. Or, I expect, because they must have gathered statistics from a big chunk of real-world (mostly C and -compatible) code and got a bit fat nothing for the usage of the overflow flag—not because it's useless but precisely because you couldn't get at it from (compiler-independent) C.
        snvzz 3y ago
        Overflow isn't the only flag RISC-V doesn't have. If floating point extensions aren't present, there aren't even flags.
        fluoridation 3y ago
        Since we're talking about implementing a compiler that merely uses C/++ as a convenient intermediate representation, it doesn't matter much.
sinkwool 3y ago
The Unison language JIT is being written in Scheme: https://www.unison-lang.org/whats-new/jit-announce/ https://www.unison-lang.org/whats-new/jit-announce/
bmitc 3y ago
I don't think the intention of Idris is to be a research language.
- retrac 3y ago
  > Idris is primarily a research project, led by Edwin Brady at the University of St Andrews, and has benefited from SICSA (https://www.sicsa.ac.uk https://www.sicsa.ac.uk) and EPSRC (https://www.epsrc.ac.uk/ https://www.epsrc.ac.uk/) funding. This does influence some design choices and implementation priorities, and means that some things are not as polished as we’d like. Nevertheless, we are still trying to make it as widely usable as we can! -- https://idris2.readthedocs.io/en/latest/faq/faq.html https://idris2.readthedocs.io/en/latest/faq/faq.html At this point, the creator has described it as "Pac-Man complete", able and easy to implement a game like Pac Man. (Or itself - it compiles to Scheme but is written in itself.) Dependent types are still rather new; I believe Idris and its libraries are one of the largest, if not the largest, body of general-purpose software that uses them. (F* maybe?) How to use dependent types properly in a standard library seems be an ongoing development.
  - Quekid5 3y ago
    The Pac-Man Complete bit is tongue-in-cheek. It's an observation that TC is rarely (if ever) actually needed in practice. (This might sound strange to people unfamiliar with dependently typed langs, but infinite streams etc., servers that "loop forever" doing request-repsonse can still be modeled without TC.)
    - mangodrunk 3y ago
      What is “TC”?
      - nextaccountic 3y ago
        Turing complete However it appears that Idris is Turing complete https://cs.stackexchange.com/questions/19577/what-can-idris-not-do-by-giving-up-turing-completeness https://cs.stackexchange.com/questions/19577/what-can-idris-... https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53dfcec086 https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53d... so I'm confused.

by retrac 3y ago

tmalsburg2 3y ago

C is neither minimal nor well-defined, as has been discussed extensively. Random blog post illustrating only some of the issues is here [1]. Just google “undefined behavior c” for a lot more. There are also a bunch of famous rants by Linus Torvalds on his topic. [1] https://blog.regehr.org/archives/213 https://blog.regehr.org/archives/213

PennRobotics 3y ago
can we all agree that the undefined behavior is pretty well identified and documented? Plus, if you understand the entire language and then limit your imagination, C can be quite simple!
- mrguyorama 3y ago
  It's so simple to avoid undefined behavior, just never add two numbers, or dereference a pointer that you can't statically guarantee the value of.
  - spookie 3y ago
    Yes, it's a simple language. That's why there are no safe guards around INT_MAX + 1, or variants of that.
  - fluoridation 3y ago
    You can add two numbers. If the operands are signed you just need to check the operands before the addition to make sure you won't cause an overflow.
    - deleted 3y ago
      [deleted]
    - johncowan 3y ago
      Which of course cannot be done portably except by drastic restrictions like "never add a number greater than MAXINT / 2 and never multiply a number greater than sqrt(MAXINT)".
      - mananaysiempre 3y ago
        Soon™ we will have ckd_add etc. in the standard for this sort of thing, after several decades finally exposing functionality that any non-exotic CPU provides. Except RISC-V, because RISC-V. Or, I expect, because they must have gathered statistics from a big chunk of real-world (mostly C and -compatible) code and got a bit fat nothing for the usage of the overflow flag—not because it's useless but precisely because you couldn't get at it from (compiler-independent) C.
        snvzz 3y ago
        Overflow isn't the only flag RISC-V doesn't have. If floating point extensions aren't present, there aren't even flags.
      - fluoridation 3y ago
        Since we're talking about implementing a compiler that merely uses C/++ as a convenient intermediate representation, it doesn't matter much.

sinkwool 3y ago

The Unison language JIT is being written in Scheme: https://www.unison-lang.org/whats-new/jit-announce/ https://www.unison-lang.org/whats-new/jit-announce/

bmitc 3y ago

I don't think the intention of Idris is to be a research language.

retrac 3y ago
> Idris is primarily a research project, led by Edwin Brady at the University of St Andrews, and has benefited from SICSA (https://www.sicsa.ac.uk https://www.sicsa.ac.uk) and EPSRC (https://www.epsrc.ac.uk/ https://www.epsrc.ac.uk/) funding. This does influence some design choices and implementation priorities, and means that some things are not as polished as we’d like. Nevertheless, we are still trying to make it as widely usable as we can! -- https://idris2.readthedocs.io/en/latest/faq/faq.html https://idris2.readthedocs.io/en/latest/faq/faq.html At this point, the creator has described it as "Pac-Man complete", able and easy to implement a game like Pac Man. (Or itself - it compiles to Scheme but is written in itself.) Dependent types are still rather new; I believe Idris and its libraries are one of the largest, if not the largest, body of general-purpose software that uses them. (F* maybe?) How to use dependent types properly in a standard library seems be an ongoing development.
- Quekid5 3y ago
  The Pac-Man Complete bit is tongue-in-cheek. It's an observation that TC is rarely (if ever) actually needed in practice. (This might sound strange to people unfamiliar with dependently typed langs, but infinite streams etc., servers that "loop forever" doing request-repsonse can still be modeled without TC.)
  - mangodrunk 3y ago
    What is “TC”?
    - nextaccountic 3y ago
      Turing complete However it appears that Idris is Turing complete https://cs.stackexchange.com/questions/19577/what-can-idris-not-do-by-giving-up-turing-completeness https://cs.stackexchange.com/questions/19577/what-can-idris-... https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53dfcec086 https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53d... so I'm confused.