The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 31/05/2013 01:46, Cody Roux wrote:
> To be fair, and I'm aware I'm getting a bit off track here, the CoC 
> already has several features that I consider "incredibly valuable to 
> know and be able to wield", at leas for PL enthusiasts:
> 
> - Higher-order functions
> - Parametric polymorphism
> - Type constructors and higher kinds
> - Dependent types

To keep things off track a bit more, I have to state that I quite don't
agree. Indeed, all you mention is fun stuff, even though the first two
points are a personal requirement to call any language "decent".

Though, looking through the Curry-Howard correspondence, I personally
consider that both on the programming side and on the logic one, the
important thing are algebraic datatypes. Without them, what you mention
is a bit dull.

1. They are a vital tool for the programmer (second order encoding is a
kludgy workaround, both for efficiency and expressivity)

2. They make logic even more exciting when you have dependent types.
Being able to express an axiom-free dependent elimination ranges from a
basic need (think of Peano's induction) to a brand new field (we're
still at the dawn of all that univalence fuss).

PMP

Attachment: signature.asc
Description: OpenPGP digital signature