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

On Mon, Sep 30, 2013 at 8:25 PM, Conal Elliott
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? Erik

| > 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
participants (2)
-
Erik Hesselink
-
Simon Peyton-Jones