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