Proposal: Don't require users to use undefined

[Christian Maeder]

Am 27.10.2010 21:57, schrieb Simon Peyton-Jones:
> | Drifting off-topic, but wouldn't we want to be able to use similar
> | syntax to bind types too? e.g.
> | 
> |     f ((Just @ t) x) = (Right @ String @ t) x
> | 
> | but @ is unavailable in patterns.
> 
> Oh yes, good point.  It'd be particularly useful in existential patterns:
> 
>   data T where
>    MkT :: forall a. a -> (a -> Int) -> T
> 
>   f (MkT @ a x g) = g (x::a)
> 
> The idea is that the pattern (MkT @ a x g) brings the type variable 'a' into scope.  As you point out, though, '@' is already used in patterns, but perhaps this use is unambiguous.  Confusing though
>    f (MkS @ a x@(p,q) z) = ....
> 
> Maybe someone else can think of good syntax.

No, I cannot, but other languages (like pvs, opal, HasCASL with
paramterized modules) use optional type arguments in square brackets
that would clash/overlap Haskell's list syntax.

I.e the function "length" could be instantiated to work on Int-Lists by
writing "length[Int]". which would have type [Int] -> Int

The problem is to distinguish "length[Int]" (of type [Int] -> Int)
from "length[True]" (of type Int) in particular for a data type like

 data Void = Void

and the term "length[Void]".

The compiler could report an ambiguity and suggest to write "length[Void
:: Void]" or "length[Void :: *]".

A type list would also bind stronger to a name than a value list.
  map length [True]   --->   (map length) [True] :: [Int]
  map length [Bool]   --->   map (length [Bool]) :: [[Bool]] -> [Int]


The next problem is the order for multiple type variables:

map f (x : xs) = f x : map f xs

Questions:
1. is an explicit type signature requires

  map :: (a -> b) -> [a] -> [b]

2. is an explicit "forall a b." needed to fix the order of the type
variables? Otherwise the order could be taken from the first occurrences
in the type signature (but would "forall b a . a -> b" then be rejected,
because the orders are contradictory?).

(Surely, the order should not be taken from the variable names like "a"
before "b".)


An instance of map is written as "map[[Int], Int] length"
(of type [[Int]] -> [Int]).

Writing "[Ty1, Ty2]" looks better to me than "[Ty1][Ty2]".

The operator "@" compared to square brackets has the disadvantage that
usually additional parens are needed to separate subsequent arguments:

  (length @ Bool) [True]

  (length @ Int) [1]

(Otherwise "Bool [True]" would be taken as wrong type.)

Also how should "map length @ Int" be parsed?

One wants "map (length @ Int)", but other infix operators (even "::")
are parsed as "(map length) @ Int".

Cheers Christian