Re: The madness of implicit parameters: cured?

2003-08-11 Thread Ashley Yakeley
At 2003-08-04 22:33, Ben Rudiak-Gould wrote:

This illustrates what you pointed out earlier, that the
program's semantics can be changed by adding explicit type signatures
which include implicitly-parameterized parameters.

But wasn't avoiding this a design goal of your proposal?

 If it is valid, then this must be a valid reduction:
 
   ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] 
 - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
   (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL 
 PROTECTED] - @x) [EMAIL PROTECTED] = 1}

Not unless you give an explicit type signature, no.

So effectively your proposal is the same as the existing implicit 
parameter mechanism, except that the compiler is a bit stricter in 
certain cases where the types are ambiguous?


-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-07 Thread Ben Rudiak-Gould
On Mon, 4 Aug 2003, Ashley Yakeley wrote:

 ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - 
 @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
 ^^^
 (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL 
 PROTECTED] - @x) [EMAIL PROTECTED] = 1}

This reduction is incorrect. The underlined parameter needs to be lifted
out, so

(\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL 
PROTECTED] - @x)

becomes

[EMAIL PROTECTED] - ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 
2})) @x)

If we next apply (\a - ...) to @x, something interesting happens: we
have to rename to avoid variable capture. I didn't realize this was ever
necessary with implicit parameters. The renaming is impossible with my
punning notation, so I'll have to write this out again with separate
interface and implementation names (yuck):

[EMAIL PROTECTED] - ((\a - ((a,[EMAIL PROTECTED] - t) [EMAIL PROTECTED] = 
2})) s)

Now names of the form @x only appear on the left hand side of {...=...}
forms, as they should, and I chose different internal names for lexically
distinct bindings. Further reduction should yield the expected answer.

The key point is that /everything/ in my proposal is lexically scoped.
That's why everything works as expected. The current system uses
quasi-dynamic scoping, which is why things work pretty much as expected
most of the time but not always.

Whenever you're in doubt about the correct way to do a reduction in my
system, do whatever preserves hygiene. And the rules for lifting implicit
parameters are isomorphic to the type-inference rules for the implicit
parameter context, so if you're ever in doubt about which parameters to
lift, figure out how the type is inferred.


 A simpler query: what types can f have here? Which if any should the 
 compiler infer?
 
   f a b = (a,b) [EMAIL PROTECTED] = 2}

Yow. The compiler certainly won't infer anything for this, but if we allow
explicit typings we get stuff like

f1 :: (Num a, Num b) = a - ((?x :: b) = b) - (a,b)
f1 a b = (a,b) [EMAIL PROTECTED] = 2}

f2 :: (Num a, Num b) = ((?x :: a) = a) - b - (a,b)
f2 a b = (a,b) [EMAIL PROTECTED] = 2}

f1 ?x ?x [EMAIL PROTECTED] = 1} == (1,2)
f2 ?x ?x [EMAIL PROTECTED] = 1} == (2,1)

This issue never occurred to me. I'd like to just ban these types, but
they look potentially useful, and in fact I see that you use them in
HScheme. I think it's up to the community to decide this one. It's sad to
lose the nice property of independence of type, but my proposal is still a
lot better than what we've got.

Note that we also have:

f0 :: (Num a, Num b) = a - b - (a,b)
f0 a b = (a,b) [EMAIL PROTECTED] = 2}   == type error: (a,b) has no parameter 
@x

f3 :: (Num a, Num b) = ((?x :: a) = a) - ((?x :: b) = b) - (a,b)
f3 a b = (a,b) [EMAIL PROTECTED] = 2}

f3 ?x ?x [EMAIL PROTECTED] = 1} == type error: (f3 ?x ?x) has no 
param. @x


 And given that type, which of these are valid?
 
   f ?x ?x
   f ?x 1
   f 1 ?x
   f 1 1

I don't think there's any way to forbid any of these while also allowing
types like those of f1 and f2 above. In fact, I don't think you can forbid
them without also forbidding

fromJust' :: (?default :: a) = Maybe a - a
fromJust' (Just x) = x
fromJust' Nothing  = ?default

I see what you're driving at, though: can/should I forbid the compiler
from inferring a type for (a,b) [EMAIL PROTECTED] = 2} under these circumstances? I
think the answer is yes, but I'm not sure. Can anyone weigh in who's
actually implemented a type inferencer for Haskell?


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-06 Thread Ben Rudiak-Gould
On Mon, 4 Aug 2003, Ashley Yakeley wrote:

 At 2003-08-04 18:19, Ben Rudiak-Gould wrote:
 
  ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] 
  - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
  ^^^
  (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL 
  PROTECTED] - @x) [EMAIL PROTECTED] = 1}
 
 This reduction is incorrect.
 
 It's a simple beta-reduction, it must be correct.

This is a different lambda calculus, with a different beta rule. You can
see the same effect in the type inference rules for implicit parameters:
If f has type Int - String and ?x has type (?x :: Int) = Int, then f ?x
has type (?x :: Int) = String, i.e. the implicit ?x parameter is lifted
out of the RHS to become a parameter of the whole application node. This
rule is what makes implicit parameters implicit.

As you pointed out, this reduction behavior depends on f's type, so this
is necessarily a typed lambda calculus. But that's okay because Haskell is
statically typed.


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-05 Thread Ben Rudiak-Gould
On Mon, 4 Aug 2003, Ashley Yakeley wrote:

 At 2003-08-04 20:00, Ben Rudiak-Gould wrote:
 
 This is a different lambda calculus, with a different beta rule. You can
 see the same effect in the type inference rules for implicit parameters:
 If f has type Int - String and ?x has type (?x :: Int) = Int, then f ?x
 has type (?x :: Int) = String, i.e. the implicit ?x parameter is lifted
 out of the RHS to become a parameter of the whole application node. This
 rule is what makes implicit parameters implicit.
 
 Ah. Actually I think the beta rule is unchanged with Haskell's implicit 
 parameters. Consider:
 
   x :: (?x :: Int) = Int
   f :: Int - String
   f :: ((?x :: Int) = Int) - ((?x :: Int) = String) -- specialisation
   f x :: (?x :: Int) = String -- apply beta rule

I think it amounts to the same thing. This is a nice way of looking at it,
though. Either way, the effect is that implicit parameters don't
disappear into function applications unless the function has been
explicitly typed to take them; instead they grow to encompass larger and
larger portions of the containing function, until eventually they become
parameters of the whole function. Result: you don't have to put them there
by hand.

 So is this valid or not?
 
   b :: (?x :: Int) = Int
   b = [EMAIL PROTECTED] - @x
 
   f :: ((?x :: Int) = Int) - (Int,Int)
   f = \a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})
 
   f b :: (Int,Int)
   f b = ((b,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})
= (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})

Yes, it is. This illustrates what you pointed out earlier, that the
program's semantics can be changed by adding explicit type signatures
which include implicitly-parameterized parameters.

 If it is valid, then this must be a valid reduction:
 
   ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] 
 - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
   (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL 
 PROTECTED] - @x) [EMAIL PROTECTED] = 1}

Not unless you give an explicit type signature, no. Without it the
compiler will infer a different type for f which does not have any
arguments with implicit parameters, because inferred types never do (see
section 2.1 in the original paper). Without this assumption the compiler
couldn't infer a principal type. (Specialization doesn't help here,
because the set of valid specializations depends on f's internals, and
can't be captured by a principal type.)


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-05 Thread Ashley Yakeley
At 2003-08-04 18:19, Ben Rudiak-Gould wrote:

 ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - 
 @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
 ^^^
 (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL 
 PROTECTED] - @x) [EMAIL PROTECTED] = 1}

This reduction is incorrect.

It's a simple beta-reduction, it must be correct.

b :: (?x :: Int) = Int
b = [EMAIL PROTECTED] - @x

f :: ((?x :: Int) = Int) - (Int,Int)
f = \a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})

f b :: (Int,Int)
f b = ((b,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})


-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-05 Thread Ben Rudiak-Gould
On Mon, 4 Aug 2003, Ashley Yakeley wrote:

 At 2003-08-04 22:33, Ben Rudiak-Gould wrote:
 
 This illustrates what you pointed out earlier, that the
 program's semantics can be changed by adding explicit type signatures
 which include implicitly-parameterized parameters.
 
 But wasn't avoiding this a design goal of your proposal?

Yes, and you convinced me that I had to give up on this goal. I'm attached
to my ideas, but only as long as they're right.


  If it is valid, then this must be a valid reduction:
  
((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL 
  PROTECTED] - @x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
(([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 
  2},[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
 
 Not unless you give an explicit type signature, no.
 
 So effectively your proposal is the same as the existing implicit 
 parameter mechanism, except that the compiler is a bit stricter in 
 certain cases where the types are ambiguous?

Yes, it's effectively the same; that was the point. I'm not trying to
create a new language extension, but an improved conceptual foundation for
the existing extension. It's fine if I don't end up with quite the design
I expected, as long as it coheres. The important thing here is the *idea*
of treating implicit parameters as a special kind of named parameter,
rather than via a problematic analogy with Lisp dynamic typing. Everything
else falls naturally (and, I hope, inevitably) out of that idea.

This idea has been very successful so far. For one thing, I just found the
solution to the monomorphism restriction problem that people have been
struggling with for as long as implicit parameters have existed. The
reason I found that answer is that my new treatment changes the design
space in such a way that the solution falls out naturally with a little
coaxing. More than anything else, this makes me think that I've hit on the
right approach to implicit parameters.


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-04 Thread Wolfgang Lux
Ben Rudiak-Gould wrote:

[...]
The final straw was:
Prelude let ?x = 1 in let g = ?x in let ?x = 2 in g
1
Prelude let ?x = 1 in let g () = ?x in let ?x = 2 in g ()
2
This is insanity. I can't possibly use a language feature which 
behaves in
such a non-orthogonal way.
Well, this is not insanity (only a little bit). In the first example, 
you
define a *value* g, i.e., g is bound to the value of ?x in its current
environment (though this value is not yet evaluated due to lazy 
evaluation),
whereas in the second example you define a function. The real insanity 
in
this point is that Haskell -- in contrast to Clean -- offers no way to
distinguish function bindings and value bindings and therefore you 
cannot
define nullary functions (except by some judicious use type signatures),
which is the heart of the monomorphism restriction mentioned by somebody
else on this list (and discussed regularly on this list :-).

Now the interesting part: I think I've managed to fix these problems. 
I'm
afraid that my solution will turn out to be just as unimplementable as 
my
original file I/O proposal, and that's very likely in this case since 
I'm
far from grokking Haskell's type system. So I'm going to present my 
idea
and let the gurus on this list tell me where I went wrong. Here we go.

[...]

Now introduce the idea of explicit named parameters to Haskell. This
requires three extensions: a new kind of abstraction, a new kind of
application, and a way of representing the resulting types.
This looks quite similar to the labeled parameters in Objective Caml. 
However,
Objective Caml's solution seems to be more general. For instance, you 
can
pass labeled parameters in arbitrary order and you can have default 
value
for optional arguments.

[...]

Why are the semantics so much clearer? I think the fundamental problem
with the existing semantics is the presence of an implicit parameter
environment, from which values are scooped and plugged into functions 
at
hard-to-predict times.
If you keep the distinction between values and functions in mind, I do 
not
think that it is hard to predict when an implicit parameter is 
substituted
(if you are willing to accept the principal problem that it is hard to
predict which value is substituted with every kind of dynamic scoping 
:-).

By substituting a notation which clearly means I
want this implicit parameter of this function bound to this value right
now, and if you can't do it I want a static type error, we avoid this
ambiguity.
IMHO, this problem were solved much easier by introducing a new syntax 
to
distinguish value and (nullary) function bindings, as was already 
repeatedly
asked for on this list in the context of the monomorphism restriction.
Personally, I'd suggest to use let x - e in ... to introduce a value 
binding
(as it is quite similar to the bindings introduced in a do-statement) 
and use
let x = e to introduce a nullary function. (I prefer - over := which 
John
Hughes and others suggested some time ago because we don't loose an 
operator
name). Thus, you example

  let ?x = 1 in let g = ?x in let ?x = 2 in g

will behave as you did expect, viz. evaluate to 2, whereas

  let ?x = 1 in let g - ?x in let ?x = 2 in g

will return 1.

Regards
Wolfgang
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-04 Thread Ben Rudiak-Gould
Trouble for implicit parameter defaults: consider

?foo = 0

let x = ?foo in
  (x + ?foo) { ?foo = 1 }

This evaluates to 1 when the monomorphism restriction is turned on, and 2
when it's off. This is no worse than the current behavior of implicit
parameters even without defaults, but I still think that it should be
forbidden because it's very important that the monomorphism restriction be
a restriction only.

This doesn't apply to defaults for explicit named parameters, but they
have their own problems: consider

#foo = 1

f :: (#foo :: a) = a
f #foo = g
g #foo = #foo

main = print ( f { #foo = 2 } :: Int )

This prints 2 if the type signature for f is included, and 1 if it's
omitted. I think this can be solved by forbidding any name with a default
from appearing more than once in any function type.

Also, reading Type classes: exploring the design space
(http://research.microsoft.com/users/simonpj/Papers/type-class-design-space/)
has given me serious doubts about explicit dictionary passing. It seems as
though it would make program behavior too dependent on otherwise minor
changes to the type inference rules.

Even without explicit dictionary passing I think you would still be able
to write

sort :: (#comparator :: a - a - Ordering) = [a] - [a]

#comparator = compare


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-04 Thread Ashley Yakeley
At 2003-08-03 14:09, Ben Rudiak-Gould wrote:

This reduction is incorrect. Auto-lifted parameters on the RHS of an
application get lifted out

I am interpreting this as Auto-lifted parameters on the RHS of an 
application get lifted out before [EMAIL PROTECTED] 'beta'-reduction can be 
done. I think this is ambiguous:

((\a - ((a,?x) [EMAIL PROTECTED] = 2})) ?x,?x) [EMAIL PROTECTED] = 1}
((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - 
@x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}

1.
(([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL 
PROTECTED] - @x) [EMAIL PROTECTED] = 1}
(([EMAIL PROTECTED] - (@x,@x)) [EMAIL PROTECTED] = 2},[EMAIL PROTECTED] - @x) [EMAIL 
PROTECTED] = 1}
((2,2),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
([EMAIL PROTECTED] - ((2,2),@x)) [EMAIL PROTECTED] = 1}
((2,2),1)

2.
([EMAIL PROTECTED] - ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) 
@x,@x)) [EMAIL PROTECTED] = 1}
((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) 1,1)
(((1,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}),1)
((([EMAIL PROTECTED] - (1,@x)) [EMAIL PROTECTED] = 2}),1)
((1,2),1)

A simpler query: what types can f have here? Which if any should the 
compiler infer?

  f a b = (a,b) [EMAIL PROTECTED] = 2}

And given that type, which of these are valid?

  f ?x ?x
  f ?x 1
  f 1 ?x
  f 1 1


-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-04 Thread Ashley Yakeley
At 2003-08-04 18:19, Ben Rudiak-Gould wrote:

   [EMAIL PROTECTED] - ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 
 2})) @x)

If we next apply (\a - ...) to @x, something interesting happens: we
have to rename to avoid variable capture.

I don't see why, isn't this much the same as ordinary names?

  (\a - ((\a - a) 1,a)) 2
  ((\a - a) 1,2)
  (1,2)


-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-04 Thread Ashley Yakeley
At 2003-08-04 20:00, Ben Rudiak-Gould wrote:

This is a different lambda calculus, with a different beta rule. You can
see the same effect in the type inference rules for implicit parameters:
If f has type Int - String and ?x has type (?x :: Int) = Int, then f ?x
has type (?x :: Int) = String, i.e. the implicit ?x parameter is lifted
out of the RHS to become a parameter of the whole application node. This
rule is what makes implicit parameters implicit.

Ah. Actually I think the beta rule is unchanged with Haskell's implicit 
parameters. Consider:

  x :: (?x :: Int) = Int
  f :: Int - String
  f :: ((?x :: Int) = Int) - ((?x :: Int) = String) -- specialisation
  f x :: (?x :: Int) = String -- apply beta rule

As you pointed out, this reduction behavior depends on f's type, so this
is necessarily a typed lambda calculus. But that's okay because Haskell is
statically typed.

So is this valid or not?

  b :: (?x :: Int) = Int
  b = [EMAIL PROTECTED] - @x

  f :: ((?x :: Int) = Int) - (Int,Int)
  f = \a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})

  f b :: (Int,Int)
  f b = ((b,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})
   = (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})

If it is valid, then this must be a valid reduction:

  ((\a - ((a,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2})) ([EMAIL PROTECTED] - 
@x),[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 1}
  (([EMAIL PROTECTED] - @x,[EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2},[EMAIL 
PROTECTED] - @x) [EMAIL PROTECTED] = 1}


-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-03 Thread Ben Rudiak-Gould
On Sat, 2 Aug 2003, Derek Elkins wrote:

 Ben Rudiak-Gould [EMAIL PROTECTED] wrote:
 
  More recently, I've realized that I really don't understand implicit
  parameters at all. They seemed simple enough at first, but when I look
  at an expression like
  
  f x = let g y = ?foo in g
  
  I realize that I have no idea what f's type should be.
 
 Do you have problems finding the type of
 
 f x = let g y = 4 in g
 ?
 it works -EXACTLY- the same way.

No, there is a big difference: There's just one dictionary value for each
type class instance, and it's global to the whole application. As a
result, it doesn't matter when hidden dictionary arguments are applied.
But implicit parameters are scoped, so it matters a lot when they're
applied. This opens up a big can of worms that the type-context system has
never had to deal with before.


 Implicit parameters aren't as flexible as full dynamic scoping would
 be.  For example,
 
 f g = let ?foo = 5 in g ()
 g x = ?foo
 
 f g :: {foo :: a) = a 
 NOT
 f g :: Num a = a
 i.e. it doesn't evaluate to 5.

But it should. Or rather, either it should evaluate to 5 or it should be a
compile-time error, because the programmer clearly thought that g within
the body of f had a implicit parameter ?foo when in fact it didn't.

In my proposal this is a type error; the message would be something like
g () does not have an implicit parameter ?foo, in the expression 'let
?foo = 5 in g ()'. It would be easy to add a helpful message to the
effect that function arguments can't have implicit parameters (which is
still true in my proposal).


  The final straw was:
  
  Prelude let ?x = 1 in let g = ?x in let ?x = 2 in g
  1
  Prelude let ?x = 1 in let g () = ?x in let ?x = 2 in g ()
  2
 
 Compare,
 
 let g = () in (g 'a' 'b',g 1 2)
 
 let g x y = x  y in (g 'a' 'b',g 1 2)

One of your expressions behaves as expected, the other is a type error.
I'm happy with both of these outcomes. But my expressions both typecheck,
but then do different things. That's scary. I was burned by this once, and
now when I try to write code with implicit parameters I have to think to
myself constantly, is this going to do what I expect? Is this going to do
what I expect?. The big selling point of functional programming is that
it makes programs easy to reason about, but implicit parameters (as
presently implemented) violate this principle to an extent that I've never
seen in any other language except Perl.


 In fact, if you use -fno-monomorphism-restriction, your examples above
 give you the same numbers.

I should point out that this is the only case in which the presence or
absence of the monomorphism restriction changes the meaning of a correct
program. In other words, it's not a restriction at all here, but an
interpretation. I hope that worries you at least a little bit.

My proposal does not behave that way: at worst, turning on the
monomorphism restriction creates an error where there was none before,
just as in the case of type class constraints.


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-03 Thread Ashley Yakeley
In article [EMAIL PROTECTED],
 Ben Rudiak-Gould [EMAIL PROTECTED] wrote:

 Now we have something almost the same as the current implicit-parameter
 system, except that it behaves in a much safer and saner way.

Hmm... you have this:

 [?x,?x] [EMAIL PROTECTED] -- OK
 [?x] [EMAIL PROTECTED] -- OK
 [] [EMAIL PROTECTED] -- not OK

You've disallowed the last one in an attempt to prevent ambiguity. 
However, not only is this ugly, it isn't sufficient. Consider this:

 let ?x = 1 in ((let g = \_ _ - ?x in let ?x = 2 in g ?x) ?x)

converts to:

 ((let g = \_ _ - [EMAIL PROTECTED] - @x in ((g ([EMAIL PROTECTED] - @x)) [EMAIL 
PROTECTED] = 2})) ([EMAIL PROTECTED] - 
@x))[EMAIL PROTECTED] = 1}

1. do  @-application first

 ((let g = \_ _ - [EMAIL PROTECTED] - @x in (g 2)) ([EMAIL PROTECTED] - @x))[EMAIL 
PROTECTED] = 1}
 (((\_ _ - [EMAIL PROTECTED] - @x) 2) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 
1}
 ((\_ - [EMAIL PROTECTED] - @x) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1}
 ([EMAIL PROTECTED] - @x)[EMAIL PROTECTED] = 1}
 1

2. do let-substitution first

 \_ _ - [EMAIL PROTECTED] - @x) ([EMAIL PROTECTED] - @x)) [EMAIL PROTECTED] = 
2}) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1}
 (((\_ - [EMAIL PROTECTED] - @x) [EMAIL PROTECTED] = 2}) ([EMAIL PROTECTED] - 
@x))[EMAIL PROTECTED] = 1}
 ((\_ - 2) ([EMAIL PROTECTED] - @x))[EMAIL PROTECTED] = 1}
 (\_ - 2) 1
 2

Again, it all depends on the type of 'g'.

-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-03 Thread Ben Rudiak-Gould
First of all, thanks for reading my proposal, and I apologize for the
ill-considered rant which preceded it. I hope you won't hold it against
me -- we should all be on the same side here.


On Sun, 3 Aug 2003, Ashley Yakeley wrote:

  ((let g = \_ _ - [EMAIL PROTECTED] - @x in ((g ([EMAIL PROTECTED] - @x)) [EMAIL 
 PROTECTED] = 2})) ([EMAIL PROTECTED] - 
 @x))[EMAIL PROTECTED] = 1}
  ((let g = \_ _ - [EMAIL PROTECTED] - @x in (g 2)) ([EMAIL PROTECTED] - 
 @x))[EMAIL PROTECTED] = 1}

This reduction is incorrect. Auto-lifted parameters on the RHS of an
application get lifted out, so

g ([EMAIL PROTECTED] - @x)  =  ([EMAIL PROTECTED] - g { @x = @x } @x)

Therefore

g ([EMAIL PROTECTED] - @x) { @x = 2 }
 = ([EMAIL PROTECTED] - g { @x = @x } @x) { @x = 2 }
 = g { @x = 2 } 2,

not (g 2) as you wrote.

Several of the other steps in your reductions are incorrect for the same
reason.

I think the following is a correct reduction, although it's easy to get
them wrong when you do them by hand:

let ?x = 1 in ((let g = \_ _ - ?x in let ?x = 2 in g ?x) ?x)
 = ((let g = \_ _ - ?x in g ?x {?x=2} ) ?x) {?x=1}
 = ((let g = \_ _ @x - @x in g ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] ) ([EMAIL 
PROTECTED] - @x)) [EMAIL PROTECTED]
 = (\_ _ @x - @x) ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED] ([EMAIL PROTECTED] - 
@x) [EMAIL PROTECTED]
 = ([EMAIL PROTECTED] - (\_ _ @x - @x) { @x = @x } @x) [EMAIL PROTECTED] ([EMAIL 
PROTECTED] - @x) [EMAIL PROTECTED]
 = (\_ _ @x - @x) [EMAIL PROTECTED] 2 ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED]
 = (\_ _ - 2) 2 ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED]
 = (\_ - 2) ([EMAIL PROTECTED] - @x) [EMAIL PROTECTED]
 = ([EMAIL PROTECTED] - (\_ - 2) @x) [EMAIL PROTECTED]
 = (\_ - 2) 1
 = 2

This is the answer I expected intuitively. If you can produce a correct
reduction which yields anything else, then I'll concede defeat. (For now.)


  [?x,?x] [EMAIL PROTECTED] -- OK
  [?x] [EMAIL PROTECTED] -- OK
  [] [EMAIL PROTECTED] -- not OK

Interesting. Can you give an example of this problem cropping up in a more
realistic context? Certainly no one will write [] [EMAIL PROTECTED], since either
it's an error or it's exactly equivalent to []. My intuition is that
this is a minor problem which would bite very rarely in practice, like
show []. And, let me emphasize again, it's safe: programs will not
silently behave in an unexpected way because of this.

By the way, I respectfully disagree that requiring explicit ?x bindings to
be used is ugly. It's an ugly additional rule in the current framework,
which treats implicit parameters as a way of simulating a Lisp-like
dynamic environment, but it's the natural state of affairs in my proposal,
which treats implicit parameters as parameters. In my proposal it's ugly
/not/ to require explicit ?x bindings to be used -- it would be like
defining (f x) to be f when f is not a function.


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-03 Thread Ben Rudiak-Gould
I just noticed something interesting. Consider

f #name = g where g #name = hello

This apparently has type (#name :: a) - (#name :: b) - String. Should
the two #names be merged? Clearly not, because ordinary positional
parameters never get merged, and named parameters are supposed to be the
same except that they're referred to by name. Then the following should be
legal:

f { #name = 1 } { #name = 2 }

So when named parameters have different names their relative order doesn't
matter, but when they have the same name it certainly does!

But this is actually a simplification, not a complication, because it
means that the distinction between positional and named parameters is a
chimera. Positional parameters behave just like named parameters having a
special out-of-band name, so ordinary abstraction and application can be
treated as sugar for named abstraction and application.

That's not quite the whole story, though:

f #name #name = #name

Is this (#name :: a) - (#name :: b) - a, or
(#name :: a) - (#name :: b) - b, or an error? This problem crops up
because my notation for abstracting named parameters involves punning
(which I hadn't noticed before): It uses the same identifier in the
interface and the implementation. The proper notation would be something
like this:

f { #name = x } { #name = y } = y

On the other hand, auto-lifted parameters with the same name clearly
should be merged. This is another way in which they differ from ordinary
named parameters, and suggests that they should indeed go in the
(unordered) type context, while ordinary named parameters clearly
shouldn't.

I don't think this is actually a problem with my proposal, but it worries
me a bit because it suggests that the semantics of named parameters aren't
quite as obvious as I previously thought.


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-03 Thread Derek Elkins
I kinda think someone mentioned this, perhaps even you.  Or maybe I'm
thinking of something else.  As I'm feeling too lazy to check the
archives, at the risk of saying something stupid or repeating something
said, you may want to look at named instances (google should turn
something up with a little effort.)  It seems to cover some of the
same issues/ideas you are having now, though in a different context.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-03 Thread Ashley Yakeley
At 2003-08-03 14:09, Ben Rudiak-Gould wrote:

  ((let g = \_ _ - [EMAIL PROTECTED] - @x in ((g ([EMAIL PROTECTED] - @x)) [EMAIL 
 PROTECTED] = 2})) ([EMAIL PROTECTED] - 
 @x))[EMAIL PROTECTED] = 1}
  ((let g = \_ _ - [EMAIL PROTECTED] - @x in (g 2)) ([EMAIL PROTECTED] - 
 @x))[EMAIL PROTECTED] = 1}

This reduction is incorrect. Auto-lifted parameters on the RHS of an
application get lifted out, so

   g ([EMAIL PROTECTED] - @x)  =  ([EMAIL PROTECTED] - g { @x = @x } @x)

Hmm... I assume you mean specifically this:

  g ([EMAIL PROTECTED] - @x)
  [EMAIL PROTECTED] - (g { @x = @x } @x)

Supposing you have this:

  g = \_ - 3

then you have this reduction:

  g ?x
  g ([EMAIL PROTECTED] - @x)
  [EMAIL PROTECTED] - (g { @x = @x } @x)
  [EMAIL PROTECTED] - ((\_ - 3) { @x = @x } @x)
  error: can't apply (\_ - 3) { @x = @x }

Something else I haven't mentioned is that you shouldn't use (-) as such 
in the type signatures. This is because (-) is an ordinary 
type-constructor. For instance, if you define this:

  type Func = (-)

then all these are the same type:

  Func a b
  (-) a b
  a - b

But in your scheme, (-) has been extended to allow certain pseudo-types 
in its first position. It might be better to use a different syntax 
rather than overload (-) with something that isn't a type-constructor.

-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-03 Thread Ben Rudiak-Gould
On Sun, 3 Aug 2003, Ashley Yakeley wrote:

 At 2003-08-03 14:09, Ben Rudiak-Gould wrote:
  g ([EMAIL PROTECTED] - @x)  =  ([EMAIL PROTECTED] - g { @x = @x } @x)
 
 Hmm... I assume you mean specifically this:
 
   g ([EMAIL PROTECTED] - @x)
   [EMAIL PROTECTED] - (g { @x = @x } @x)
 
 Supposing you have this:
 
   g = \_ - 3

Yeah, the application rule is actually more complicated than that: it
depends on knowing all the auto-lifted parameters of both the LHS and the
RHS. The set of autolifted parameters of the application node is the union
of these two sets, and each parameter is passed on only to the function(s)
that need it. This means that in a dynamically-typed implementation,
application is necessarily quite strict: both the LHS and the RHS need to
be reduced to HNF, whereas normally you need only WHNF on the LHS and
nothing on the RHS. However, I don't think this is a problem in Haskell,
since all the necessary information can be derived statically from the
type.

 Something else I haven't mentioned is that you shouldn't use (-) as such 
 in the type signatures. This is because (-) is an ordinary 
 type-constructor.

Okay, good point. (=) seems like the obvious choice. I shall use it
henceforth.


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


Re: The madness of implicit parameters: cured?

2003-08-03 Thread Ben Rudiak-Gould
On Sun, 3 Aug 2003, Derek Elkins wrote:

 I kinda think someone mentioned this, perhaps even you.  Or maybe I'm
 thinking of something else.  As I'm feeling too lazy to check the
 archives, at the risk of saying something stupid or repeating something
 said, you may want to look at named instances (google should turn
 something up with a little effort.)  It seems to cover some of the
 same issues/ideas you are having now, though in a different context.


I found a paper on named instances at

http://www.cs.uu.nl/people/ralf/hw2001/4.html

Thanks for pointing me to this; it's very interesting. As part of my
proposal I was thinking about the possibility of decoupling the typeclass
system from implicitness, but there were enough complications that I gave
up. But this paper makes it look doable.

Given plus :: (Num a) = a - a - a, the application plus (1::Int)
currently has type Int - Int. But it could equally well have type
(Num Int) = Int - Int. This type has the advantage of being more
versatile: in principle you can supply your own type class. The problem is
that usually you want Int - Int, and it would be terribly cumbersome to
have to apply the default Num Int dictionary by hand every time. That's as
far as I got.

But the paper points out that implicit context reduction in this case is
perfectly safe and predictable as long as there's a global default value
for the dictionary. Two implicit reductions can't conflict because the
value passed implicitly is always the same, and an implicit reduction
can't conflict with an explicit one because the explicit reduction changes
the type, making the implicit reduction illegal. The paper suggests the
notation f # MyInstance, but of course I think it should be something like
f { Num Int = MyInstance } or f { MyInstance }. This notation is uglier,
but it's more consistent and it avoids stealing a nice short infix
operator which people have proposed to use for many other things.

This works for named parameters too (explicit and implicit). You could
write something like

default #name = value

or even just

#name = value

since this introduces no ambiguity if named parameters never clash with
ordinary variable identifiers. Then implicit reduction is perfectly safe
(in the sense that the behavior is unaffected by type signatures). This is
better than the parameter-defaulting scheme I was thinking of.

There are some complications, but I think they all have solutions:

1. The default value for #name has to be global to the whole application,
   so functions in other modules with a named parameter #name will have to
   use your default. Solution: make parameter names part of the module
   namespace.

2. You can't have named parameters with the same name but different types,
   if there's a global default. Solution: Invent a new notation for
   explicitly typing the defaults (not sure this is possible), or just
   live with the limitation. Haskell doesn't have Java-style overloading.

3. Problems arise in the case of duplicate dictionary types. Consider
   f x y = (x+1,y+1) with type (Num a, Num b) = a - b - (a,b).
   Then g = f (1::Int) (2::Int) has type (Num Int, Num Int) = (Int,Int).
   In the expression g { Num Int = ... }, which typeclass parameter are we
   applying? The solution, as pointed out in the paper, is to make the
   typeclass parameters explicit in the definition of f. Then f has type
   Num a = Num b = ... and g has type Num Int = Num Int = (Int,Int),
   and the order of application is unambiguous.

There are additional subtleties described in the paper which I don't
understand yet.


-- Ben

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell


The madness of implicit parameters: cured?

2003-08-02 Thread Ben Rudiak-Gould
When I first learned about implicit parameters I thought they were a great
idea. The honeymoon ended about the time I wrote some code of the form
let ?foo = 123 in expr2, where expr2 used ?foo implicitly, and debugging
eventually unearthed the fact that ?foo's implicit value was not being set
to 123 in expr2. That was enough to scare me off of using implicit
parameters permanently.

More recently, I've realized that I really don't understand implicit
parameters at all. They seemed simple enough at first, but when I look at
an expression like

f x = let g y = ?foo in g

I realize that I have no idea what f's type should be. Is it

(?foo :: c) = a - b - c

or is it

a - ((?foo :: c) = b - c)

? As far as I can tell, these are not the same type: you can distinguish
between them by partially applying f with various different values of ?foo
in the implicit environment. GHC tells me that f has the former type, but
I still have no idea why: is it because g has an implicit ?foo parameter
and f implicitly applies its own ?foo to g before returning it? Why would
it do that? Or is it because ?foo is here interpreted as referring to an
implicit parameter bound in the call of f, instead of in g? That doesn't
make sense either.

The final straw was:

Prelude let ?x = 1 in let g = ?x in let ?x = 2 in g
1
Prelude let ?x = 1 in let g () = ?x in let ?x = 2 in g ()
2

This is insanity. I can't possibly use a language feature which behaves in
such a non-orthogonal way.

Now the interesting part: I think I've managed to fix these problems. I'm
afraid that my solution will turn out to be just as unimplementable as my
original file I/O proposal, and that's very likely in this case since I'm
far from grokking Haskell's type system. So I'm going to present my idea
and let the gurus on this list tell me where I went wrong. Here we go.

First, discard the current implicit-parameter scheme entirely. (I'll
eventually build up to something very similar.)

Now introduce the idea of explicit named parameters to Haskell. This
requires three extensions: a new kind of abstraction, a new kind of
application, and a way of representing the resulting types.

The abstraction could be done with a new lambda form, but instead I'll use
a special prefix on identifiers which are to be considered named
parameters, namely the character #. The new application form will be
[F] { #x = [G] } where [F] and [G] are expressions. [F] must evaluate to a
function with an explicit named parameter #x.

The type notation for a named parameter will be (#name :: type). They can
appear only on the left side of a -. Named parameters can only be passed
by name, so their order relative to positional parameters and each other
doesn't matter; therefore we may as well bubble them up to the head of
the list of arguments. In fact, we could put them in the context with the
type classes, but I won't do so.

Examples:

cons :: (#elem :: a) - (#list :: [a]) - [a]
cons #elem #list = #elem : #list

cons { #elem = 'h', #list = ello }-- legal

cons 'h' ello -- illegal: named params must be passed by name

cons { #list = ello } -- legal, has type (#elem :: Char) - String

cons { #list = ello, #elem = 'h' }-- legal

cons { #list = ello } { #elem = 'h' } -- legal

append :: (#right :: [a]) - [a] - [a]
append left #right = ...-- named args gravitate left

Now introduce the idea of auto-lifted named parameters. I'll distinguish
these from ordinary named parameters by using an @ prefix instead of #.
These are exactly the same as ordinary named parameters except that if
they appear in the type on the right hand side of an application node,
they are implicitly lifted to the whole node. For example, if [F] has an
auto-lifted parameter @p, and [G] has auto-lifted parameters @p and @q,
then [F][G] is implicitly converted to something like
[EMAIL PROTECTED] @q - [F] { @p = @p } ( [G] { @p = @p, @q = @q } ).

Finally, introduce the following syntax:

* As an expression, ?x is short for [EMAIL PROTECTED] - @x.

* On the left hand side of the = sign in a named application, ?x is
  the same as @x.

* For backward compatibility, let ?x = [E] in [F] should be treated
  as equivalent to [F] { ?x = [E] }.

Now we have something almost the same as the current implicit-parameter
system, except that it behaves in a much safer and saner way.

For example, looking at the confusing expressions from the beginning again:

f x = let g y = ?foo in g

This obviously has type (?foo :: c) - a - b - c. It doesn't
matter where the ?foo parameter appears in the type because it will
always be referred to explicitly, by name, exactly once in each
call of f.

let ?x = 1 in let g = ?x in let ?x = 2 in g

This reduces as follows:

  let ?x = 1 in let g = ?x in let ?x = 2 in g
  ( let g = [EMAIL PROTECTED] - @x in g { @x = 2 } ) { @x = 1 }

Re: The madness of implicit parameters: cured?

2003-08-02 Thread Derek Elkins
On Sat, 2 Aug 2003 00:45:07 -0700 (PDT)
Ben Rudiak-Gould [EMAIL PROTECTED] wrote:

 When I first learned about implicit parameters I thought they were a
 great idea. The honeymoon ended about the time I wrote some code of
 the formlet ?foo = 123 in expr2, where expr2 used ?foo implicitly,
 and debugging eventually unearthed the fact that ?foo's implicit value
 was not being set to 123 in expr2. That was enough to scare me off of
 using implicit parameters permanently.
 
 More recently, I've realized that I really don't understand implicit
 parameters at all. They seemed simple enough at first, but when I look
 at an expression like
 
 f x = let g y = ?foo in g
 
 I realize that I have no idea what f's type should be. Is it
 
 (?foo :: c) = a - b - c
 
 or is it
 
 a - ((?foo :: c) = b - c)

Do you have problems finding the type of

f x = let g y = 4 in g
?
it works -EXACTLY- the same way.

 
 ? As far as I can tell, these are not the same type: you can
 distinguish between them by partially applying f with various
 different values of ?foo in the implicit environment. 

If you do apply f you get (?foo :: c) = b - c.

GHC tells me
 that f has the former type, but I still have no idea why: is it
 because g has an implicit ?foo parameter and f implicitly applies its
 own ?foo to g before returning it? Why would it do that? Or is it
 because ?foo is here interpreted as referring to an implicit parameter
 bound in the call of f, instead of in g? That doesn't make sense
 either.

The constraint should just be thought of as an extra explicit
parameter, or think of it as using the same mechanism dictionary
passing for type classes uses. Implicit parameters aren't
as flexible as full dynamic scoping would be.  For example,

f g = let ?foo = 5 in g ()
g x = ?foo

f g :: {foo :: a) = a 
NOT
f g :: Num a = a
i.e. it doesn't evaluate to 5.  So you can't bind the free implicit
variables of a passed in HOF (basically you can't have type ({?foo :: t
= a - t) - b), and similarly you can't return HOF's with free
implicit parameters (no type a - ({?foo :: t = t - b))

If I'm not way rusty with CL, here are similar examples with full
dynamic scoping,
 (defvar *x* 0)
*X*
 (defun f (g) (let ((*x* 5)) (funcall g)))
F
 (defun g () *x*)
G
 (f #'g)
5
 (defun f (x) (defun g (y) *x*))
F
 (let ((*x* 1)) (f 'a))
G
 (funcall * 'b)
0
 (let ((*x* 2)) (funcall ** 'b))
2


 The final straw was:
 
 Prelude let ?x = 1 in let g = ?x in let ?x = 2 in g
 1
 Prelude let ?x = 1 in let g () = ?x in let ?x = 2 in g ()
 2
 
 This is insanity. I can't possibly use a language feature which
 behaves in such a non-orthogonal way.

Compare,

let g = () in (g 'a' 'b',g 1 2)

let g x y = x  y in (g 'a' 'b',g 1 2)

the problem with this is again -EXACTLY- the same because implicit
parameters behave very much like class constraints, because class
constraints pretty much ARE implicit parameters.  The problem here is
the monomorphism restriction.  This applies to implicit parameters as
well for the same reasons (and because implicit
parameters are very likely handled by the same code.)  In fact, if you
use -fno-monomorphism-restriction, your examples above give you the same
numbers.
   ___ ___ _
  / _ \ /\  /\/ __(_)
 / /_\// /_/ / /  | |  GHC Interactive, version 5.04.3
/ /_\\/ __  / /___| |  http://www.haskell.org/ghc/
\/\/ /_/\/|_|  Type :? for help.

Loading package base ... linking ... done.
Loading package haskell98 ... linking ... done.
Prelude :set -fglasgow-exts
Prelude let ?x = 1 in let g = ?x in let ?x = 2 in g
1
Prelude let ?x = 1 in let g () = ?x in let ?x = 2 in g ()
2
Prelude :set -fno-monomorphism-restriction
Prelude let ?x = 1 in let g = ?x in let ?x = 2 in g
2
Prelude let ?x = 1 in let g () = ?x in let ?x = 2 in g ()
2

Whether your additions would be worthwhile anyways, I haven't really
thought about.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell