Taral wrote:

On 9/11/06, Bulat Ziganshin wrote:

...

Expr Bool = Eq (Expr t) (Expr t) | forall t . Eq t

Still confusing, but less so.

The problem is that it's really backwards. The symbol being defined is "Eq". Eq (Expr t) (Expr t) | Eq t = Expr Bool

but that doesn't fit well, does it? In my mind, the current mode is a functional one:

Eq :: Eq t => Expr t -> Expr t -> Expr Bool

And this is perfectly readable. The arrow means that the argument is an implicit propositional one, but it's still an argument.

Perhaps the proposed new style of function signature could also be used in a GADT eg: -- There is no need for the keyword "Data" because we know it's part of -- a GADT because the function name is a conid - all such decls in a module would -- then be gathered together to form the GADT(s) If :: Expr Bool -> Expr t -> Expr t -> Expr t Eq :: Expr t -> Expr t -> Expr Bool | Eq t Lit :: Int -> Expr Int or data Expr t = If (Expr Bool) (Expr t) (Expr t) Expr Bool = Eq (Expr t) (Expr t) | Eq t Expr Int = Lit Int The second option is of course backwards compared to a function declaration, but this is natural because there can only ever be one clause for each value constructor but mutiple clauses per result type, whereas in a function decl there can be multiple clauses for each pattern but only one result type, therefore function decls are inherently backwards wrt data decls... Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com

Taral wrote:

On 9/11/06, Bulat Ziganshin wrote:

...

Expr Bool = Eq (Expr t) (Expr t) | forall t . Eq t

Still confusing, but less so.

The problem is that it's really backwards. The symbol being defined is "Eq". Eq (Expr t) (Expr t) | Eq t = Expr Bool

but that doesn't fit well, does it?

You could also argue that the symbol being defined is the tycon "Expr", since a data decl defines both a tycon and zero or more value constructors. This leads to a symmetric relationship: to define a type we write multiple clauses for the same tycon and to define a function we write multiple clauses for the same function name. The clauses for each tycon are "used" at compile time to find value constructors for the corresponding type, and the clauses for each function name are "used" at run time to find values for the corresponding function application.

In my mind, the current mode is a functional one:

Eq :: Eq t => Expr t -> Expr t -> Expr Bool

And this is perfectly readable. The arrow means that the argument is an implicit propositional one, but it's still an argument.

The => arrow ties the concept of restricted quantification to the concept of passing implicit arguments around behind the scenes. Is this desireable? It is also worth mentioning that the bar syntax allows for better interactive syntax highlighting in an editor, because putting the quantifier after the type means there is no ambiguity when parsing left to right - when we get to a '|' we know what follows is a quantifier (restricted or unrestricted) whereas in the current => syntax an editor can't tell that the user is typing parts of a context until the whole context has already been typed - too late to provide interactive feedback! ;-) Tomasz Zielonka wrote:

On Sun, Sep 10, 2006 at 10:08:22AM +0400, Bulat Ziganshin wrote:

...

sequence :: [m a] -> m [a] | Monad m

I am not entirely sure, but I think this syntax for type class context is used in the Concurrent Clean language.

Some examples can be found in the Clean report 2.0 Dec 2001 eg page 59. Regards, Brian. -- Logic empowers us and Love gives us purpose. Yet still phantoms restless for eras long past, congealed in the present in unthought forms, strive mightily unseen to destroy us. http://www.metamilk.com