[ghc-steering-committee] Proposal: Syntax for visible dependent quantification (#81)

[Joachim Breitner]

Hi,

thanks for the recommendation.

Am Mittwoch, den 20.12.2017, 20:35 +0000 schrieb Roman Leshchinskiy:
> If we decide to discuss just the proposal as is, though, then I'd be
> weakly against the proposed syntax as it is too subtle for my taste
> and abuses familiar mathematical notation somewhat. I'd probably
> prefer something like:
> 
>   type a -> t

I am not saying that the proposed “forall a ->” syntax is great, but I
think it is still better than “type a -> …”. The reason is that we
already use prefixing “type”, e.g. in export lists (“type Bool”), to
say “this thing is a type” if there is ambiguity. So if anything, then

  ifThenElse :: Bool -> a -> a -> a

should be also allowed to be written as

  ifThenElse :: type Bool -> a -> a -> a

and hence, in consequence

  ifThenElse :: type Bool -> type a -> type a -> a

In other words, “type foo” just clarifies “I mean the _type_ foo”.


Can we get more input?

> Because of this, my recommendation is to strongly encourage the author
> to submit an extended proposal which reserves (but doesn't specify the
> semantics of) the above syntax wholesale.

I’d be on board deciding on that syntax all in one go.

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/20180105/c0ebe7c6/attachment.sig>