• simonpj's avatar
    [project @ 2001-11-29 13:47:09 by simonpj] · 32a89583
    simonpj authored
    	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
    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)
    		      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)
    	 		 (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.
    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)
    		      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)
    		      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.