Membership relation

[anshwad10]

I also found an example in Cubical.Functions.Embedding where it would make the code easier to understand, and there are probably many more situations

[felixwellen]

Judging from experience with similar definitions, it is not a good idea to use a unicode version of an already existing symbol like ":". Otherwise I very much sympathize with what you are suggesting here. Maybe you could find a different syntax? Maybe this is something which would be better changed on the side of Agda (opinions @andreasabel )?

[anshwad10]

Well, \in is already used by Powerset, and :: is already used by lists. Should I open an issue on the agda repo to make it built in? Haskell already does that with ::, so I don't think it'll be too difficult to add it.

[felixwellen]

Let's just wait a bit to see if Andreas has a comment. This must have been discussed in the past.

[felixwellen]

Well, \in is already used by Powerset, and :: is already used by lists. Should I open an issue on the agda repo to make it built in? Haskell already does that with ::, so I don't think it'll be too difficult to add it.

There should be an easy hacky implementation (using just the regular ":") which changes the parser to generally allow it and just uses your definition in a desugaring phase. But that should be horrible error-message wise.

[andreasabel]

Maybe this is something which would be better changed on the side of Agda (opinions @andreasabel )?

We have discussed type annotations on and off in the past; I am pro, but there has not been a watertight proposal how to add them yet.
Just using the colon for type annotations (which is the natural path to go) does clash in the syntax of dependent function types, e.g.

(A : Set) -> A

would become ambiguous:

1. What it means now: quantification over A : Set, so this is the empty type.
2. A -> A where the domain is annotated with its universe, Set.

[anshwad10]

I think this should be fine, because even TypeTopology does this (and they happen to use the same notation that I chose as well)

[anshwad10]

I remember some other library using the ∋ symbol for this, but I can't seem to recall which one it was.

[anshwad10]

(A : Set) -> A would become ambiguous:

1. What it means now: quantification over A : Set, so this is the empty type.
2. A -> A where the domain is annotated with its universe, Set.

What about letting (A : Set) -> A mean the first, but (_ : A : Set) -> A mean the second? I don't think there will be much use for the second anyways.

[andreasabel]

There is also opportunities to misread (A × B : C) -> (A : C)...

[felixwellen]

Yes... And it makes sense to not confuse two things which are actually different. A binder/declaration of a variable "x : A" (happy to be corrected on terminology) is different from a type-annotated term "t : A". I think the latter should have a notation which suggests that there is really just an annotation and the whole thing is still an expressen/a term. Maybe "t :< A >" or something like that.

[felixwellen]

Ah, okay. On the other hand, these two things are already notated the same in Agda and more generally in type theory.

[anshwad10]

I remember some other library using the ∋ symbol for this, but I can't seem to recall which one it was.

Ah, it was the agda standard library

[felixwellen]

There is also opportunities to misread (A × B : C) -> (A : C)...

On second thought, I'm not sure I get the point. The first ": C" should be good, since we would give ":" the lowest priority possible, so it is an annotation here. Is the problem that "A : C" could be a variable? Then it is an instance of the same problem as above.
Can the latter be resolved by disallowing shadowing in this situation? (Maybe that would be horrible from an engineering perspective)

[andreasabel]

There is also opportunities to misread (A × B : C) -> (A : C)...

While brain 2 can sort it out correctly, brain 1 might be tripped up by the visual similarity between typed binding and type annotation.

[felixwellen]

@mortberg what do you think?

[felixwellen]

Or @ecavallo ?

[ecavallo]

I don't have a strong opinion in any direction. There are definitely situations where I've wanted something like this (don't remember any specifically, but similar to the example in the PR).

How about t :> A as a syntax?

The ambiguous situations for : seem unlikely to come up in real life. But I agree with Felix that using a unicode symbol that looks like : will be confusing.

[felixwellen]

I'd be happy with t :> A. Should also be easy to replace if we ever have a better idea.

[anshwad10]

@ecavallo

How about t :> A as a syntax?

Good idea!