type equality symbol

[Isaac Dupree]

Simon Peyton-Jones wrote:
> | > Nothing deep.  Just that "=" means so many things that it seemed better
> | > to use a different notation.
> | >
> |
> | How about ==? Only one meaning so far, and that both on the term level and
> | equivalent to the constraint
> 
> I'm quite happy with "~"!  It's sufficiently different from "=" that someone
 > meeting it for the first time is going to thing "hmm, better read the 
manual";
 > and they'd be right.

I think this is the most important distinction: whether they will need 
to read the manual.  I suppose it usually doesn't need to be written 
explicitly, so when it is, manual-reading (or a comment in the code) 
would be more likely to be important.

(also (==) is generally a non-reserved symbol, though that could perhaps 
be changed like forall's (.))

> Anyway, while on this subject, I am considering making the following change:
> 
>         make all operator symbols into type constructors
>         (currently they are type variables)
> 
> That would allow you to write
>         data a * b = Prod a b
>         data a + b = Left a | Right b
> and write natural-looking types like
>         f :: a*b -> a
> 
> When we have indexed type families working, this will be even more natural.
> 
> As things stand, only operators starting with a ":" are type constructors, thus
>         data a :*: b = Prod a b
> etc.  By analogy with the term language, operators are currently classified as "type variables", so you could write (oddly)
>         data T (+) x = MkT (+) x
> [this may not even work today, but it should] to mean the same as
>         data T y x = MkT y x
> But this is pretty useless!  Very occasionally one might want a type variable
 > with kind (*->*->*), but much much more often you want a type 
*constructor* with that kind.

I've seen "~>" after (Arrow (~>)) =>, as a type variable... and find it 
confusing!  for the (unimplementable)
reverseArrow :: (Arrow a) => a b c -> a c b
sometimes written as
reverseArrow :: (Arrow (~>)) => (b ~> c) -> (c ~> b)
, I'd prefer, if infix notation is going to be used, the backtick 
version for variables (as well as being allowed for types e.g. (b `SF` c))
reverseArrow :: (Arrow a) => (b `a` c) -> (c `a` b)

Also, '->' doesn't start with a colon.  (and is currently 
lowest-precedence, the way (::) in expressions is? or do we know what 
we're doing with precedences/associativity?  To give infix declaration 
explicitly, must define (+)-type in a different module than (+)-value if 
it's different fixity...)

I support that (+)-etc-as-type-constructor change!

(hmm, is there any additional difficulty in it if experimenting with 
language features mixing type and term expressions - which already has 
lexical ambiguity anyway?)

Isaac