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

[Joachim Breitner]

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/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180326/b73e8d48/attachment.sig>