3 ms·

Why would you use Twelf over Agda? Honest question—I've never examined Twelf.

by tel 13y ago

CountHackulus 13y ago
Same question, but for Idris. I've found that Idris is quite easy to understand and looks similar to Agda.
- tel 13y ago
  I find Idris has a more computational flair while Agda is often "done after typechecking". Idris doesn't enforce termination as strictly as Agda. Idris' interactive modes are less friendly and powerful—Agda's emacs mode is best in breed. Idris has typeclasses and Agda something akin to first-class modules (as stated above). That's a fairly big difference. Idris handles laziness and strictness (or, relatedly, data/codata) a little differently than Agda, but it's not a huge concern until you get technical. Idris is also just younger than Agda and subsequently works a little wonkily. Again I find this exposed through the interactive mode which sometimes provides rather strange information. Although honestly that happens in both Agda and Idris. Idris has nice syntax for embedded DSLs which is demonstrated in its Effects library which would be possible to replicate in Agda but not as nice looking. One big difference is that Agda uses universe polymorphism and Idris uses cumulative universes. This shows up in a lot of parameterization of Set in Agda. If you find Idris easy to understand than Agda will be absolutely no harder. Go take a look at the Agda standard library to get a taste: https://github.com/agda/agda-stdlib https://github.com/agda/agda-stdlib Something like Relation.Binary.Core is a good place to start: https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/Core.agda https://github.com/agda/agda-stdlib/blob/master/src/Relation...
jonsterling 13y ago
Most of the things I want to do end up meaning that I need a logical framework in which to build a type theory. I use Agda for that, but this is not its strength (try building a non-trivial term language with binding, for instance).
- tel 13y ago
  I never realized it could be much easier than Agda, but I've been playing with Twelf now for a little bit and am getting a feel for how LF and HOAS work together.

Why would you use Twelf over Agda? Honest question—I've never examined Twelf.

by tel 13y ago

Why would you use Twelf over Agda? Honest question—I've never examined Twelf.

CountHackulus 13y ago

Same question, but for Idris. I've found that Idris is quite easy to understand and looks similar to Agda.

tel 13y ago
I find Idris has a more computational flair while Agda is often "done after typechecking". Idris doesn't enforce termination as strictly as Agda. Idris' interactive modes are less friendly and powerful—Agda's emacs mode is best in breed. Idris has typeclasses and Agda something akin to first-class modules (as stated above). That's a fairly big difference. Idris handles laziness and strictness (or, relatedly, data/codata) a little differently than Agda, but it's not a huge concern until you get technical. Idris is also just younger than Agda and subsequently works a little wonkily. Again I find this exposed through the interactive mode which sometimes provides rather strange information. Although honestly that happens in both Agda and Idris. Idris has nice syntax for embedded DSLs which is demonstrated in its Effects library which would be possible to replicate in Agda but not as nice looking. One big difference is that Agda uses universe polymorphism and Idris uses cumulative universes. This shows up in a lot of parameterization of Set in Agda. If you find Idris easy to understand than Agda will be absolutely no harder. Go take a look at the Agda standard library to get a taste: https://github.com/agda/agda-stdlib https://github.com/agda/agda-stdlib Something like Relation.Binary.Core is a good place to start: https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/Core.agda https://github.com/agda/agda-stdlib/blob/master/src/Relation...

jonsterling 13y ago

Most of the things I want to do end up meaning that I need a logical framework in which to build a type theory. I use Agda for that, but this is not its strength (try building a non-trivial term language with binding, for instance).

tel 13y ago
I never realized it could be much easier than Agda, but I've been playing with Twelf now for a little bit and am getting a feel for how LF and HOAS work together.