should flat be off by default?

[HuStmpHrrr]

it is strange to me that flat is on by default. I always think of Agda's type system as something around MLTT but the flat modality itself seems kicking it off the range. I am wondering why flat is on by default? I would expect a special option to turn it on as it is an addon feature.

[nad]

We have discussed this before. I am not opposed to a flag.

[Saizan]

You need special syntax for it, and it doesn't add to the power of the type system unless you postulate things.

[jespercockx]

You need special syntax for it, and it doesn't add to the power of the type system unless you postulate things.

The same is true for Prop (at least if you already have irrelevance), yet somehow it's still hidden under a flag.

[Saizan]

I thought Prop was under a flag because of backwards incompatibilities wrt inference?

[Saizan]

Irrelevance itself does not need a flag btw, and it's not something you have in plain MLTT.

[nad]

I would not mind having a flag for irrelevance as well.

In order to make it easier to fix broken code I suggest that we do not add such flags until #3118 has been implemented.

[HuStmpHrrr]

I would say we should have flags for every addon features.

[jespercockx]

In order to make it easier to fix broken code I suggest that we do not add such flags until #3118 has been implemented.

It is now implemented, so go nuts with adding more flags I guess ;)

[nad]

I noticed that the type Cohesion has three constructors:

agda/src/full/Agda/Syntax/Common.hs

Lines 1338 to 1345 in bd2afa1

	-- | Cohesion modalities
	-- see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584)
	-- types are now given an additional topological layer which the modalities interact with.
	data Cohesion
	= Flat -- ^ same points, discrete topology, idempotent comonad, box-like.
	| Continuous -- ^ identity modality.
	-- | Sharp -- ^ same points, codiscrete topology, idempotent monad, diamond-like.
	| Squash -- ^ single point space, artificially added for Flat left-composition.

Should the flag for turning off this modality be called --flat, --cohesion, or something else? If it is called --cohesion, then it could perhaps be used also for the sharp modality, which is commented out above, if support for such a modality is added in the future (#5459).

@plt-amy suggested that one could refuse to parse @flat/@♭ unless the flag is on. Given that there are three constructors, does that suffice? There is only syntax for Flat:

agda/src/full/Agda/Syntax/Concrete/Attribute.hs

Lines 90 to 94 in bd2afa1

	cohesionAttributeTable :: [(String, Cohesion)]
	cohesionAttributeTable =
	[ ("♭" , Flat)
	, ("flat" , Flat)
	]

The default seems to be Continuous:

agda/src/full/Agda/Syntax/Common.hs

Lines 1493 to 1495 in bd2afa1

	-- | Identity under composition
	unitCohesion :: Cohesion
	unitCohesion = Continuous

agda/src/full/Agda/Syntax/Common.hs

Lines 1501 to 1503 in bd2afa1

	-- | Default Cohesion is the identity element under composition
	defaultCohesion :: Cohesion
	defaultCohesion = unitCohesion

Can one guarantee that Squash will never interfere with anything just by not parsing Flat? Note that Squash is part of zeroModality:

agda/src/full/Agda/Syntax/Common.hs

Lines 1489 to 1491 in bd2afa1

	-- | 'Cohesion' forms a monoid under addition, and even a semiring.
	zeroCohesion :: Cohesion
	zeroCohesion = Squash

agda/src/full/Agda/Syntax/Common.hs

Lines 500 to 502 in bd2afa1

	-- | Identity under addition
	zeroModality :: Modality
	zeroModality = Modality zeroRelevance zeroQuantity zeroCohesion

[nad]

I added --cohesion.

[plt-amy]

Well, aiui Squash is just what Continuous becomes when we go into a Flat context, right? Are there any other cases where we apply zeroModality to the context?