[Agda] Identifying experimental Agda features for Cabal support

[Nils Anders Danielsson]

On 2009-09-22 13:26, Darin Morrison wrote:
> I'd like to revive the discussion started at AIM 10 about which
> features should be enabled by default in Agda and which should be
> marked as experimental or as language extensions.

> To get the discussion started, a quick proposal of language extensions
> might look like the following:
> 
> Coinduction
> InductiveFamilies
> InductionRecursion
> SizedTypes
> UniversePolymorphism

Some questions/observations:

* For the benefit of those of us who missed AIM 10, can you explain what
  the rationale for classifying a feature as a language "extension" is?

* How should features be enabled? Using LANGUAGE pragmas, like in
  Haskell?

* If a user does not trust a given feature, then I suppose (s)he would
  want to ensure that the feature is never used in a given development.
  In Haskell there is no easy way to enforce this. Do we want
  project-wide disabling of features to be easy? In that case I think it
  should also be easy to ensure that code does not use postulates, does
  not turn off the termination checker, etc.

* Inductive families are so integral to Agda 2 that it would seem quite
  strange to label them as an extension.

* You may want to add some features to your list: FFI, records, with,
  optimised constraint solving for constructor-headed functions…

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.