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
