[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.

1 files changed, 8 insertions, 15 deletions

diff --git a/ghc/compiler/types/TypeRep.lhs b/ghc/compiler/types/TypeRep.lhs
index 8e2002c24a..bb0a7f01b4 100644
--- a/ghc/compiler/types/TypeRep.lhs
+++ b/ghc/compiler/types/TypeRep.lhs
@@ -6,7 +6,7 @@
 \begin{code}
 module TypeRep (
 	Type(..), TyNote(..), 		-- Representation visible 
-	SourceType(..), IPName(..),	-- to friends
+	SourceType(..), 		-- to friends
 	
  	Kind, PredType, ThetaType,		-- Synonyms
 	TyVarSubst,
@@ -29,13 +29,13 @@ module TypeRep (
 #include "HsVersions.h"
 
 -- friends:
-import Var	( TyVar )
-import VarEnv
-import VarSet
-
-import Name	( Name )
-import TyCon	( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
-import Class	( Class )
+import Var	  ( TyVar )
+import VarEnv     ( TyVarEnv )
+import VarSet     ( TyVarSet )
+import Name	  ( Name )
+import BasicTypes ( IPName )
+import TyCon	  ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
+import Class	  ( Class )
 
 -- others
 import PrelNames	( superKindName, superBoxityName, liftedConName, 
@@ -213,13 +213,6 @@ data SourceType
   | NType TyCon [Type]		-- A *saturated*, *non-recursive* newtype application
 				-- [See notes at top about newtypes]
 
-data IPName name
-  = Dupable   name	-- ?x: you can freely duplicate this implicit parameter
-  | MustSplit name	-- %x: you must use the splitting function to duplicate it
-  deriving( Eq, Ord )	-- Ord is used in the IP name cache finite map
-			--	(used in HscTypes.OrigIParamCache)
-	-- I sometimes thisnk this type should be in BasicTypes
-		
 type PredType  = SourceType	-- A subtype for predicates
 type ThetaType = [PredType]
 \end{code}