[project @ 2001-11-29 13:47:09 by simonpj]
------------------------------ Add linear implicit parameters ------------------------------ Linear implicit parameters are an idea developed by Koen Claessen, Mark Shields, and Simon PJ, last week. They address the long-standing problem that monads seem over-kill for certain sorts of problem, notably: * distributing a supply of unique names * distributing a suppply of random numbers * distributing an oracle (as in QuickCheck) Linear implicit parameters are just like ordinary implicit parameters, except that they are "linear" -- that is, they cannot be copied, and must be explicitly "split" instead. Linear implicit parameters are written '%x' instead of '?x'. (The '/' in the '%' suggests the split!) For example: data NameSupply = ... splitNS :: NameSupply -> (NameSupply, NameSupply) newName :: NameSupply -> Name instance PrelSplit.Splittable NameSupply where split = splitNS f :: (%ns :: NameSupply) => Env -> Expr -> Expr f env (Lam x e) = Lam x' (f env e) where x' = newName %ns env' = extend env x x' ...more equations for f... Notice that the implicit parameter %ns is consumed once by the call to newName once by the recursive call to f So the translation done by the type checker makes the parameter explicit: f :: NameSupply -> Env -> Expr -> Expr f ns env (Lam x e) = Lam x' (f ns1 env e) where (ns1,ns2) = splitNS ns x' = newName ns2 env = extend env x x' Notice the call to 'split' introduced by the type checker. How did it know to use 'splitNS'? Because what it really did was to introduce a call to the overloaded function 'split', ndefined by class Splittable a where split :: a -> (a,a) The instance for Splittable NameSupply tells GHC how to implement split for name supplies. But we can simply write g x = (x, %ns, %ns) and GHC will infer g :: (Splittable a, %ns :: a) => b -> (b,a,a) The Splittable class is built into GHC. It's defined in PrelSplit, and exported by GlaExts. Other points: * '?x' and '%x' are entirely distinct implicit parameters: you can use them together and they won't intefere with each other. * You can bind linear implicit parameters in 'with' clauses. * You cannot have implicit parameters (whether linear or not) in the context of a class or instance declaration. Warnings ~~~~~~~~ The monomorphism restriction is even more important than usual. Consider the example above: f :: (%ns :: NameSupply) => Env -> Expr -> Expr f env (Lam x e) = Lam x' (f env e) where x' = newName %ns env' = extend env x x' If we replaced the two occurrences of x' by (newName %ns), which is usually a harmless thing to do, we get: f :: (%ns :: NameSupply) => Env -> Expr -> Expr f env (Lam x e) = Lam (newName %ns) (f env e) where env' = extend env x (newName %ns) But now the name supply is consumed in *three* places (the two calls to newName,and the recursive call to f), so the result is utterly different. Urk! We don't even have the beta rule. Well, this is an experimental change. With implicit parameters we have already lost beta reduction anyway, and (as John Launchbury puts it) we can't sensibly reason about Haskell programs without knowing their typing. Of course, none of this is throughly tested, either.
Showing with 385 additions and 243 deletions