[Agda] Identifying experimental Agda features for Cabal support

[Darin Morrison]

On Tue, Sep 22, 2009 at 9:19 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:

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

I think the main rationale was that some people were worried that
packages would start showing up using features which not everyone was
comfortable with using.  Certain things in Agda at the moment are
clearly more experimental and less well understood than others, for
example the codata/coinduction stuff.  If people can agree upon a
subset of Agda which they "trust" (maybe "understand" is better), then
features which fall outside of this subset can be considered as
"extensions" for the time being.

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

This is one way, yes.  The other way (which is what I had in mind) is
to specify the features in the Cabal file.  For example, something
like the following:

executable agda-pkg
  extensions:       FlexibleInstances
                  , GeneralizedNewtypeDeriving
                  , MultiParamTypeClasses
                  , OverloadedStrings

> * 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.

Yes, this was also discussed.  It seems that people do want this
functionality.  I don't think it would be hard to add this to the Agda
cabal support.  All one needs to do is store a field for packages in
the database specifying which extensions they used and then check this
information during dependency analysis to determine whether
undesirable features will be used.

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

Personally I agree.  Also they are used quite heavily in the current
library.  I only listed it because it was mentioned at least once
during the meeting :)

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

FFI I could potentially see on the list but maybe the others are too
fine-grained and nobody seemed to complain about them anyway.

-- 
Darin