4 ms·

Hey, this is out of the University of St.Andrews! I went there! During my time they were a big Haskell shop, working with Glasgow University (the G in ghc). Th

Hey, this is out of the University of St.Andrews! I went there! During my time they were a big Haskell shop, working with Glasgow University (the G in ghc). There were also into custom research languages that nobody's ever heard of like Napier and, erm, S-Algol (again with Glasgow; the S stands for 'Scottish')... I see that Idris generates real machine code. I see it goes through LLVM, so the code quality should be decent; but I see a reference that the binary needs to know where the compiler is, which makes me a bit worried about the needed dependencies. Additionally, apart from the dependent types, does Idris fix some of the annoyances with Haskell --- modules, namespacing, field access, shudder strings?

chrisseaton 10y ago
> the code quality should be decent Using LLVM requires that your code is in pretty decent shape before it goes in, really. LLVM is great for replacing your own actual instruction selection, scheduling and assembly, but you can't generate LLVM IR naively from a high-level language and expect LLVM to do anything sensible with it. You seem to basically need a language-specific IR and optimisation passes before you start to think about emitting LLVM. See Rubinius - it implemented a Ruby JIT using LLVM and is often slower than the standard Ruby interpreter!
billytrend 10y ago
RE S-Algol, it actually stands for St Andrews Algol. I developed a javascript transpiler as my final year project (2016) which is incomplete but there are some working examples here: https://goo.gl/TjbwML https://goo.gl/TjbwML . I found the project fascinating. Of course this a completely different language to Idris, the only real relation is that it was also developed in St Andrews.
- david-given 10y ago
  I could have sworn it was 'Scottish', because that meant that the language wasn't entirely St.Andrews' fault, but it was nearly twenty years ago... At the time I quite liked it, and did a lot of programming in the SunOS version (the one where they hadn't gotten around to writing the garbage collector). I know better now, of course. Tell me, do you still cringe when you hear the phrase 'void and void are not compatible in this context'?
  - billytrend 10y ago
    Aha that's probably wishful thinking I'm afraid. The language seemed very old fashioned to me (features like being able to choose the first index of an array) but I can appreciate it was good for its time. I wrote my own error messages which were hopefully a bit more useful than that :)
infinisil 10y ago
Yes! - Idris' `String` type is not just a list of characters, here [1] you can see some relevant functions, I'm still trying to find the definition of `String` though. - Functions can be overloaded in Idris, which enables declaring a field with the same name on different records. I'm not sure what you mean with modules and namespacing though [1] https://www.idris-lang.org/docs/current/prelude_doc/docs/Prelude.Strings.html https://www.idris-lang.org/docs/current/prelude_doc/docs/Pre...
- efnx 10y ago
  Idris has namespacing instead of modules, which is great and allows for things like locally scoped data declarations
nouv 10y ago
I'm a current student here, imagine my surprise reading a top comment on HN talking about St Andrews!

chrisseaton 10y ago

> the code quality should be decent Using LLVM requires that your code is in pretty decent shape before it goes in, really. LLVM is great for replacing your own actual instruction selection, scheduling and assembly, but you can't generate LLVM IR naively from a high-level language and expect LLVM to do anything sensible with it. You seem to basically need a language-specific IR and optimisation passes before you start to think about emitting LLVM. See Rubinius - it implemented a Ruby JIT using LLVM and is often slower than the standard Ruby interpreter!

billytrend 10y ago

RE S-Algol, it actually stands for St Andrews Algol. I developed a javascript transpiler as my final year project (2016) which is incomplete but there are some working examples here: https://goo.gl/TjbwML https://goo.gl/TjbwML . I found the project fascinating. Of course this a completely different language to Idris, the only real relation is that it was also developed in St Andrews.

david-given 10y ago
I could have sworn it was 'Scottish', because that meant that the language wasn't entirely St.Andrews' fault, but it was nearly twenty years ago... At the time I quite liked it, and did a lot of programming in the SunOS version (the one where they hadn't gotten around to writing the garbage collector). I know better now, of course. Tell me, do you still cringe when you hear the phrase 'void and void are not compatible in this context'?
- billytrend 10y ago
  Aha that's probably wishful thinking I'm afraid. The language seemed very old fashioned to me (features like being able to choose the first index of an array) but I can appreciate it was good for its time. I wrote my own error messages which were hopefully a bit more useful than that :)

infinisil 10y ago

Yes! - Idris' `String` type is not just a list of characters, here [1] you can see some relevant functions, I'm still trying to find the definition of `String` though. - Functions can be overloaded in Idris, which enables declaring a field with the same name on different records. I'm not sure what you mean with modules and namespacing though [1] https://www.idris-lang.org/docs/current/prelude_doc/docs/Prelude.Strings.html https://www.idris-lang.org/docs/current/prelude_doc/docs/Pre...

efnx 10y ago
Idris has namespacing instead of modules, which is great and allows for things like locally scoped data declarations

nouv 10y ago

I'm a current student here, imagine my surprise reading a top comment on HN talking about St Andrews!