Re: The madness of implicit parameters: cured?
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 = \@x -> @x f :: ((?x :: Int) => Int) -> (Int,Int) f = \a -> ((a,\@x -> @x) {@x = 2}) f b :: (Int,Int) f b = ((b,\@x -> @x) {@x = 2}) = ((\@x -> @x,\@x -> @x) {@x = 2}) If it is valid, then this must be a valid reduction: ((\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1} ((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 1} -- Ashley Yakeley, Seattle WA
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 = \@x -> @x
f :: ((?x :: Int) => Int) -> (Int,Int) f = \a -> ((a,\@x -> @x) {@x = 2})
f b :: (Int,Int) f b = ((b,\@x -> @x) {@x = 2}) = ((\@x -> @x,\@x -> @x) {@x = 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,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1} ((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 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
participants (2)
-
Ashley Yakeley -
Ben Rudiak-Gould