4 ms·

not the most powerful system imaginable for that purpose had to ask, what is more powerful, agda/coq/other?

• evincarofautumn 15y ago
  A full dependent type system is nominally “the most powerful system imaginable”, but it’s also hopelessly problematic. You can’t be sure that type inference or type checking will halt in the general case, although you can infer some value-dependent types (see “Dependent Type Inference with Interpolants” by Unno & Kobayashi). In practice this means you need manifest type signatures, otherwise the type of a function would be “lol iunno ¯\(°_o)/¯”. Then again, Haskell requires signatures in some cases, such as for Rank-N types, or when you run up against the Dread Monomorphism Restriction. So yeah, Agda and Coq are awesome, but most useful as what they’re designed to be—proof assistants—rather than general-purpose languages. tl;dr: A constrained system such as Haskell’s, with extensions for aspects of dependent typing, is more practical than actual dependent typing.
  • gtani 15y ago
    just googled/bookmarked: http://www.cs.princeton.edu/~dpw/papers/TCS04.pdf http://www.cs.princeton.edu/~dpw/papers/TCS04.pdf http://www.metaocaml.org/concoqtion/techreport.pdf http://www.metaocaml.org/concoqtion/techreport.pdf http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pierce.pdf http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pier... slide 8: summary = impossible