A flag for "Simple Agda"?

[jespercockx]

This Mastodon post by William Bowman gave me the idea that it could be nice to have a flag for "Simple Agda" which disables all of the advanced syntax and type features that might be confusing to people just learning Agda. This would emphatically not be aimed at serious "power users" of Agda but rather at people who use Agda to learn more about type theory.

Here are some things the flag could do:

• Disable universe polymorphism (= --no-universe-polymorphism)
• Disable instance arguments
• Disable copattern matching (and perhaps disable record types altogether)
• Disable named implicit arguments (i.e. only allow passing them by position)
• Disable generalizable variables
• Disable anonymous modules (and maybe disable parametrized modules altogether)
• Disable named where blocks
• Disable all modalities such as irrelevance and erasure
• Disable pattern-matching lambdas
• Disable mixfix operators other than binary operations (with perhaps an exception for if_then_else_)
• Disable unicode syntax (with perhaps a few exceptions for very common characters)

[gallais]

These look like linting rules to me. Could it be implemented as a standalone program using the Agda parser as a library?

[jespercockx]

Two more proposals by David Thrane Christiansen on Mastodon:

• Disable eta-equality for records (if we don't remove them completely)
• Enable --exact-split

[jespercockx]

These look like linting rules to me. Could it be implemented as a standalone program using the Agda parser as a library?

I suppose they could, though it would be nice if there was some way to plug this into Agda's interactive mode so you can get the warnings/errors right in your editor when you load the file.

[andreasabel]

• Disable named implicit arguments (i.e. only allow passing them by position)

Or rather: disable positional implicit arguments (only allow passing them by name). 😜

[jespercockx]

Or rather: disable positional implicit arguments (only allow passing them by name). 😜

I see a lot of newcomers getting confused by the {x = x} syntax, so I'm not sure if that would be a good idea.

[pigworker]

Copatterns make Agda simpler! The notation should be extended! The assumption that we only ever do a bunch of left stuff then a bunch of right stuff has been problematic forever. With does something about that but not enough. Copatterns do something about that but not enough. Mutter mutter sequent calculus not natural deduction.

[jespercockx]

These look like linting rules to me. Could it be implemented as a standalone program using the Agda parser as a library?

See also https://github.com/agda/agda/issues/7008

[jespercockx]

Copatterns make Agda simpler! The notation should be extended! The assumption that we only ever do a bunch of left stuff then a bunch of right stuff has been problematic forever. With does something about that but not enough. Copatterns do something about that but not enough. Mutter mutter sequent calculus not natural deduction.

They do, but they are still one of the most common points that people ask about / are confused about when coming from Haskell. Since they are not part of MLTT and not common in other languages, I think we should perhaps be pragmatic.

[pigworker]

It will not surprise you at all that I think people coming from Haskell should not be overly indulged. I think our entire community has suffered from Haskell drag, making things more awkward in order to be less scary. "simple" should not be code for "reinforcing of the old misconceptions".

[jwaldmann]

... making things more awkward in order to be less scary.

I (coming from Haskell, mostly) am genuinely interested in examples of such "things" so I can recognize them, and avoid them - when writing, or teaching, Agda.

[pigworker]

Let's start with data types. They're generative, and they don't have first class descriptions: you can't compute a data type, e.g., by differentiating another one. Worse, we lose the power to program when we're saying which data might exist, which is a pity, as we have so much information (the indices of the data type) to program with. The data type notation has just bumbled along the same way functional languages have always done it.

A particular consequence of this absence of first class computable data type descriptions is that we struggle to achieive "found" functoriality, traversability, etc. You can't point out that a particular unparametrized data type is, in fact, functorial in some of the stuff it packs up. People do outrageous type class programming to sort of bully GHC into walking through a Foo frobbing all the Bars, instead of saying "by the way, Foo is Blah[Bar/X]; traverse the Blah".

[xekoukou]

We should not use datatypes. I dont know how. Maybe make them private and force people to create records of their structure and properties?

[jamesmckinna]

It's a separate thread, but (a long time ago) a blog post by Frank Atanassow (TODO: find article maybe on LtU?) was very critical of the turn towards dependent types in programming, precisely because of the 'inevitability' of exposing too much structure/implementation via pattern-matching, and thus the encouragement to violate abstraction (barriers).

I think 'we' still haven't (pace the desire for a 'simple Agda') developed a good way to cash out the old-skool signature/structure distinction for dependently-typed APIs, precisely because we end up... having to reify definitional equalities in implementation with propositional/setoid ones in specification (just as SML, at least as far as teaching it was concerned, got stymied by sharing constraints), and despite interesting work by Magaud and Bertot at the beginning of this century on that problem (and perhaps, the idiomatic use of views for representation change, modulo --with-K... how does that go down with the students?), I think there's still a long way to go. But very happy to be pointed at more recent work if it is out there!

[jespercockx]

I think 'we' still haven't (pace the desire for a 'simple Agda') developed a good way to cash out the old-skool signature/structure distinction for dependently-typed APIs

I agree that this is still an open problem, opaque is the most recent attempt at tackling it. But the holy grail of being able to abstract over definitional equalities is still a way off.