Symbolic type variables (was Re: [Proposal] Renaming (:=:) to (==))

[Simon Peyton-Jones]

| > I'm hoping we don't get more deeply invested in the syntactic change
| in GHC
| > 7.6 that removed the possibility of symbolic type variables ("~>",
| "*", "+",
| > etc). I had a new job and wasn't paying attention when SPJ polled the
| > community. From my perspective, the loss has much greater scope than
| the
| > gain for type level naturals. I'd like to keep the door open to the
| > possibility of bringing back the old notation with the help of a
| language
| > pragma. It would take a few of us to draft a proposal addressing
| details.
| 
| I also miss these on a regular basis. I seem to remember that during
| the proposal, there was a mention of reversing the situation, i.e.
| having a prefix for type variable operators instead. Did anything ever
| come of that?

I'm very open to concrete suggestions about this. I want Haskell to allow you to express the thoughts in your head, as directly as possible.

We could add a LANGUAGE pragma.  Or, more radically, we could support both at once, like this:

	data (&&) a b where ...blah blah...
	f :: Int && Int -> Bool
	f = ...
	
	data T (&&) x = MkT (x && x)
	-- Shadows (&&)

The idea is that (&&) can be declared as a top-level type constructor, but then *shadowed* by an explicit local binding in the 'data T' declaration. This is somewhat analogous to the situation with values:
	f = True
	g f = f::Char
where we define f globally and then shadow it.

The apparent difference is that the top-level (&&) is a type constructor, whereas the local (&&) is a type variable; and in the value world we *never* shadow data constructors.

But the counter-argument might be that type variables (unlike term variables) really do behave like type constructors: they are rigid and don't match anything else.

So I think the door stands open here, if anyone wants to drive the debate and push it through to a consensus.

Simon