[ghc-steering-committee] Proposal: Binding existential type variables (#96)

[Richard Eisenberg]

I've had a similar idea. However, Simon once convinced me that we would want some syntactic distinction between inputs and outputs: otherwise a reader of code wouldn't differentiate variable occurrences from variable bindings.

For example:

f x y = case y of P x x -> ...

Note that I haven't given the type of P. In the pattern there, is the first x an occurrence while the second a new binding that shadows the outer x? Or is the first x a binding and the second one an occurrence? Or are they both occurrences? (They can't both be bindings!) A type system could, in theory, sort this out, but then the renamer behavior would have to depend on types. And it's terribly confusing for readers.

So if we want to consider this future extension, we should have a syntactic marker for the inputs. Perhaps using * would remind C programmers of dereferencing:

f x y = case y of P *x x -> ...

Now it's all very clear! (Well, maybe not *very* clear.) But we can unambiguously say that the first x is an occurrence of the outer x and the second is a binding site of a shadowing variable.

Bringing this back to the proposal at hand, we would say this to mention a universal:

g (Just *@Int x) = x

and that would mean g :: Maybe Int -> Int

Of course, these little syntactic sigils make Haskell look more Perlish, and that's not a good thing.

Richard

> On Mar 26, 2018, at 2:22 PM, Joachim Breitner <mail at joachim-breitner.de> wrote:
> 
> Hi,
> 
> I know that it is frowned upon to discuss the merits of one proposal
> with hypothetical future proposals in mind, but I can’t resist:
> 
> Am Montag, den 26.03.2018, 12:44 -0400 schrieb Richard Eisenberg:
>> 3. Like Simon, I see the value in being able to say that everything
>> that occurs in a pattern is a pattern -- that is, an output of the
>> match.
> 
> I wonder if raising this current state to a principle blocks us from
> very useful future extensions. In particular, I expect that in the
> future we will want to be able to abstract pattern synonyms over
> values, and be able to do something like the following, given in
> infeasible syntax.
> 
>  pattern Nths n x <- ((!! ns) -> x)
> 
>  squareTenth :: [Int] -> Int
>  squareTenth (Nths 10 x) = x*x
> 
> or
> 
>  nths :: Int -> [a] -> a
>  nths n (Nths n x) = x
> 
> 
> Ah, and of course view patterns already break the rule that “everything
> that occurs in a pattern is a pattern”!
> 
> 
> So somewhere down the line, I expect that patterns with have both INPUT
> and OUTPUT terms, and I will be able to specify both. In the same vain,
> I would like to be able to specify both INPUT and OUTPUT types now.
> 
> 
> And just in case this is a course of confusion: Nobody proposes to
> _bind_ universal variables. But Romand and me are missing a way of
> explicitly _instantiating_ universal variables. The proposal only
> discuss the former (which I agree is bogus), but not the latter.
> 
> 
> 
> Cheers,
> Joachim
> 
> 
> -- 
> Joachim Breitner
>  mail at joachim-breitner.de
>  http://www.joachim-breitner.de/
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee