[Agda] Identifying experimental Agda features for Cabal support

[Patrik Jansson]

Darin Morrison skrev:
> Hi All,
>
> 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.
>
> I think it's important to reach a consensus about this soon so that I
> can add support for enabling/disabling these features in the Agda
> cabal support, which I'm hoping can make it into the next Cabal/GHC
> release (coming up in the next few weeks as I understand).
>
> To get the discussion started, a quick proposal of language extensions
> might look like the following:
>
> Coinduction
> InductiveFamilies
> InductionRecursion
> SizedTypes
> UniversePolymorphism
>
> One might also want to include options to disable various checks:
>
> NoPositivityCheck
> NoTerminationCheck
> TypeInType
>
> although maybe the latter shouldn't receive special treatment and
> should just be specified as extra command line options.  Conceptually,
> I don't think they are really language extensions so much as compiler
> options.
>
> I'm of the opinion that it would be best to start off as conservative
> as possible regarding which features are defaulted so that people
> really know what they are getting when they use an Agda package from
> someone else.  Also, it's a lot easier to start off conservative and
> change things later than the other way around once a large number of
> packages have already been written.
>
> Thoughts?
>   
Conservative sounds OK to me, but I suspect some of the above may be a 
bit difficult to implement properly. So the pragmatic way would be to 
jump in and try to implement support of a few of the "extensions" (which 
are rather "restrictions" of the current default) and see which can be 
done reasonably easily.

/Patrik

> --
> Darin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>