sem.icl

   1 implementation module sem
   2
   3 import qualified Data.Map as Map
   4
   5 from Data.Func import $
   6 from StdFunc import o, flip, const, id
   7
   8 import Control.Applicative
   9 import Control.Monad
  10 import Control.Monad.Trans
  11 import Control.Monad.State
  12 import Data.Either
  13 import Data.Maybe
  14 import Data.Monoid
  15 import Data.List
  16 import Data.Functor
  17 import Data.Tuple
  18
  19 import StdString
  20 import StdTuple
  21 import StdList
  22 import StdMisc
  23 import StdEnum
  24 import GenEq
  25
  26 from Text import class Text(concat), instance Text String
  27
  28 import AST
  29
  30 :: Scheme = Forall [TVar] Type
  31 :: Gamma :== 'Map'.Map String Scheme //map from Variables! to types
  32 :: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
  33 :: Substitution :== 'Map'.Map TVar Type
  34 :: Constraints :== [(Type, Type)]
  35 :: SemError
  36         = ParseError Pos String
  37         | UnifyError Pos Type Type
  38     | InfiniteTypeError Pos Type
  39     | FieldSelectorError Pos Type FieldSelector
  40         | OperatorError Pos Op2 Type
  41     | UndeclaredVariableError Pos String
  42     | ArgumentMisMatchError Pos String
  43         | SanityError Pos String
  44         | Error String
  45
  46 instance zero Gamma where
  47         zero = 'Map'.newMap
  48
  49 variableStream :: [TVar]
  50 variableStream = map toString [1..]
  51
  52 defaultGamma :: Gamma //includes all default functions
  53 defaultGamma = extend "print" (Forall ["a"] ((IdType "a") ->> VoidType))
  54                 $ extend "isEmpty" (Forall ["a"] ((ListType (IdType "a")) ->> BoolType))
  55                 $ extend "read" (Forall [] (FuncType CharType))
  56                 $ extend "1printchar" (Forall [] (CharType ->> VoidType))
  57                 $ extend "1printint" (Forall [] (IntType ->> VoidType))
  58                 $ extend "1printbool" (Forall [] (BoolType ->> VoidType))
  59                 zero
  60
  61 sem :: AST -> Either [SemError] (AST, Gamma)
  62 sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
  63                         >>| foldM (const isNiceMain) () fd
  64                         >>| hasMain fd
  65                     >>| runStateT (unfoldLambda fd >>= type) (defaultGamma, variableStream) of
  66         Left e = Left [e]
  67     Right ((_,fds),(gam,_)) = Right (AST fds, gam)
  68 where
  69                 hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
  70                 hasNoDups fds (FunDecl p n _ _ _ _)
  71                 # mbs = map (\(FunDecl p` n` _ _ _ _)->if (n == n`) (Just p`) Nothing) fds
  72                 = case catMaybes mbs of
  73                         [] = Left $ SanityError p "HUH THIS SHOULDN'T HAPPEN"
  74                         [x] = pure ()
  75                         [_:x] = Left $ SanityError p (concat
  76                                 [n, " multiply defined at ", toString p])
  77
  78                 hasMain :: [FunDecl] -> Either SemError ()
  79                 hasMain [(FunDecl _ "main" _ _ _ _):fd] = pure ()
  80                 hasMain [_:fd] = hasMain fd
  81                 hasMain [] = Left $ SanityError zero "no main function defined"
  82
  83                 isNiceMain :: FunDecl -> Either SemError ()
  84                 isNiceMain (FunDecl p "main" as mt _ _) = case (as, mt) of
  85                         ([_:_], _) = Left $ SanityError p "main must have arity 0"
  86                         ([], t) = (case t of
  87                                 Nothing = pure ()
  88                                 Just VoidType = pure ()
  89                                 _ = Left $ SanityError p "main has to return Void")
  90                 isNiceMain _ = pure ()
  91
  92
  93 //------------------
  94 // LAMBDA UNFOLDING
  95 //------------------
  96 unfoldLambda :: [FunDecl] -> Typing [FunDecl]
  97 unfoldLambda [] = pure []
  98 unfoldLambda [fd:fds] = unfoldL_ fd >>= \(gen1, fs_)->
  99                         unfoldLambda fds >>= \gen2->
 100                         pure $ gen1 ++ [fs_] ++ gen2
 101
 102 flattenT :: [([a],b)] -> ([a],[b])
 103 flattenT ts = (flatten $ map fst ts, map snd ts)
 104
 105 class unfoldL_ a :: a -> Typing ([FunDecl], a)
 106
 107 instance unfoldL_ FunDecl where
 108     unfoldL_ (FunDecl p f args mt vds stmts) =
 109         flattenT <$> mapM unfoldL_ vds >>= \(fds1,vds_) ->
 110         flattenT <$> mapM unfoldL_ stmts >>= \(fds2,stmts_)->
 111         pure (fds1 ++ fds2, FunDecl p f args mt vds_ stmts_)
 112
 113 instance unfoldL_ VarDecl where
 114     unfoldL_ (VarDecl p mt v e) = unfoldL_ e >>= \(fds, e_)->pure (fds, VarDecl p mt v e_)
 115
 116 instance unfoldL_ Stmt where
 117     unfoldL_ (IfStmt e th el) = unfoldL_ e >>= \(fds, e_)->pure (fds, IfStmt e_ th el)
 118     unfoldL_ (WhileStmt e c) = unfoldL_ e >>= \(fds, e_)->pure (fds, WhileStmt e_ c)
 119     unfoldL_ (AssStmt vd e) = unfoldL_ e >>= \(fds, e_)->pure (fds, AssStmt vd e_)
 120     unfoldL_ (FunStmt f es fs) = flattenT <$> mapM unfoldL_ es >>= \(fds, es_)->
 121         pure (fds, FunStmt f es_ fs)
 122     unfoldL_ (ReturnStmt (Just e)) = unfoldL_ e >>= \(fds, e_) ->
 123         pure (fds, ReturnStmt (Just e_))
 124     unfoldL_ (ReturnStmt Nothing) = pure ([], ReturnStmt Nothing)
 125
 126 instance unfoldL_ Expr where
 127     unfoldL_ (LambdaExpr p args e) =
 128         fresh >>= \(IdType n) ->
 129         let f = ("lambda_"+++n) in
 130         let fd = FunDecl p f args Nothing [] [ReturnStmt $ Just e] in
 131         let fe = FunExpr p f [] [] in
 132         pure ([fd], fe)
 133     unfoldL_ (FunExpr p f es fs) = flattenT <$> mapM unfoldL_ es >>= \(fds, es_)->
 134         pure (fds, FunExpr p f es_ fs)
 135     unfoldL_ e = pure ([], e)
 136
 137 //------------
 138 //------------
 139 //      TYPING
 140 //------------
 141 //------------
 142
 143 class Typeable a where
 144     ftv :: a -> [TVar]
 145     subst :: Substitution a -> a
 146
 147 instance Typeable Scheme where
 148     ftv (Forall bound t) = difference (ftv t) bound
 149     subst s (Forall bound t) = Forall bound $ subst s_ t
 150         where s_ = 'Map'.filterWithKey (\k _ -> not (elem k bound)) s
 151
 152 instance Typeable [a] | Typeable a where
 153     ftv types   = foldr (\t ts-> ftv t ++ ts) [] types
 154     subst s ts  = map (\t->subst s t) ts
 155
 156 instance Typeable Type where
 157     ftv (TupleType (t1, t2))    = ftv t1 ++ ftv t2
 158     ftv (ListType t)            = ftv t
 159     ftv (IdType tvar)           = [tvar]
 160     ftv (FuncType t)            = ftv t
 161     ftv (t1 ->> t2)             = ftv t1 ++ ftv t2
 162     ftv _                       = []
 163     subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2)
 164     subst s (ListType t1)       = ListType (subst s t1)
 165     subst s (FuncType t)        = FuncType (subst s t)
 166     subst s (t1 ->> t2)         = (subst s t1) ->> (subst s t2)
 167     subst s t1=:(IdType tvar)   = 'Map'.findWithDefault t1 tvar s
 168     subst s t                   = t
 169
 170 instance Typeable Gamma where
 171     ftv gamma       = concatMap id $ map ftv ('Map'.elems gamma)
 172     subst s gamma   = Mapmap (subst s) gamma
 173
 174 extend :: String Scheme Gamma -> Gamma
 175 extend k t g = 'Map'.put k t g
 176
 177 //// ------------------------
 178 //// algorithm U, Unification
 179 //// ------------------------
 180 instance zero Substitution where zero = 'Map'.newMap
 181
 182 compose :: Substitution Substitution -> Substitution
 183 compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1
 184 //Note: just like function compositon compose does snd first
 185
 186 occurs :: TVar a -> Bool | Typeable a
 187 occurs tvar a = elem tvar (ftv a)
 188
 189 unify :: Type Type -> Either SemError Substitution
 190 unify t1 t2=:(IdType tv)    | t1 == (IdType tv) = Right zero
 191                             | occurs tv t1 = Left $ InfiniteTypeError zero t1
 192                             | otherwise = Right $ 'Map'.singleton tv t1
 193 unify t1=:(IdType tv) t2 = unify t2 t1
 194 unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1->
 195                                 unify ta2 tb2 >>= \s2->
 196                                 Right $ compose s1 s2
 197 unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1->
 198                                                     unify ta2 tb2 >>= \s2->
 199                                                     Right $ compose s1 s2
 200 unify (ListType t1) (ListType t2) = unify t1 t2
 201 unify (FuncType t1) (FuncType t2) = unify t1 t2
 202 unify t1 t2 | t1 == t2  = Right zero
 203             | otherwise = Left $ UnifyError zero t1 t2
 204
 205 //// ------------------------
 206 //// Algorithm M, Inference and Solving
 207 //// ------------------------
 208 gamma :: Typing Gamma
 209 gamma = gets fst
 210 putGamma :: Gamma -> Typing ()
 211 putGamma g = modify (appFst $ const g) >>| pure ()
 212 changeGamma :: (Gamma -> Gamma) -> Typing Gamma
 213 changeGamma f = modify (appFst f) >>| gamma
 214 withGamma :: (Gamma -> a) -> Typing a
 215 withGamma f = f <$> gamma
 216 fresh :: Typing Type
 217 fresh = gets snd >>= \vars->
 218         modify (appSnd $ const $ tail vars) >>|
 219         pure (IdType (head vars))
 220
 221 lift :: (Either SemError a) -> Typing a
 222 lift (Left e) = liftT $ Left e
 223 lift (Right v) = pure v
 224
 225 //instantiate maps a schemes type variables to variables with fresh names
 226 //and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d]
 227 instantiate :: Scheme -> Typing Type
 228 instantiate (Forall bound t) =
 229     mapM (const fresh) bound >>= \newVars->
 230     let s = 'Map'.fromList (zip (bound,newVars)) in
 231     pure (subst s t)
 232
 233 //generalize quentifies all free type variables in a type which are not
 234 //in the gamma
 235 generalize :: Type -> Typing Scheme
 236 generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t
 237
 238 lookup :: String -> Typing Type
 239 lookup k = gamma >>= \g-> case 'Map'.member k g of
 240     False = liftT (Left $ UndeclaredVariableError zero k)
 241     True = instantiate $ 'Map'.find k g
 242
 243 //The inference class
 244 //When tying it all together we will treat the program is a big
 245 //let x=e1 in let y=e2 in ....
 246 class infer a :: a -> Typing (Substitution, Type, a)
 247
 248 ////---- Inference for Expressions ----
 249
 250 instance infer Expr where
 251  infer e = case e of
 252     VarExpr _ (VarDef k fs) = lookup k >>= \t ->
 253         foldM foldFieldSelectors t fs >>= \finalT ->
 254         pure (zero, finalT, e)
 255
 256     Op2Expr p e1 op e2 =
 257         infer e1 >>= \(s1, t1, e1_) ->
 258         infer e2 >>= \(s2, t2, e2_) ->
 259         fresh >>= \tv ->
 260         let given = t1 ->> t2 ->> tv in
 261         op2Type op >>= \expected ->
 262         lift (unify expected given) >>= \s3 ->
 263         pure ((compose s3 $ compose s2 s1), subst s3 tv, Op2Expr p e1_ op e2_)
 264
 265     Op1Expr p op e1 =
 266         infer e1 >>= \(s1, t1, e1_) ->
 267         fresh >>= \tv ->
 268         let given = t1 ->> tv in
 269         op1Type op >>= \expected ->
 270         lift (unify expected given) >>= \s2 ->
 271         pure (compose s2 s1, subst s2 tv, Op1Expr p op e1)
 272
 273     EmptyListExpr _ = (\tv->(zero,tv,e)) <$> fresh
 274
 275     TupleExpr p (e1, e2) =
 276         infer e1 >>= \(s1, t1, e1_) ->
 277         infer e2 >>= \(s2, t2, e2_) ->
 278         pure (compose s2 s1, TupleType (t1,t2), TupleExpr p (e1_,e2_))
 279
 280     LambdaExpr _ _ _ = liftT $ Left $ Error "PANIC: lambdas should be Unfolded"
 281
 282     FunExpr p f args fs =
 283         lookup f >>= \expected ->
 284         let accST = (\(s,ts,es) e->infer e >>= \(s_,et,e_)-> pure (compose s_ s,ts++[et],es++[e_])) in
 285         foldM accST (zero,[],[]) args >>= \(s1, argTs, args_)->
 286         fresh >>= \tv->case expected of
 287             FuncType t = pure (s1, t, e)
 288             _ = (let given = foldr (->>) tv argTs in
 289                 lift (unify expected given) >>= \s2->
 290                 let fReturnType = subst s2 tv in
 291                 foldM foldFieldSelectors fReturnType fs >>= \returnType ->
 292                 (case f of
 293                     "print" = case head argTs of
 294                         IntType = pure "1printint"
 295                         CharType = pure "1printchar"
 296                         BoolType = pure "1printbool"
 297                         ListType (CharType) = pure "1printstr"
 298                         t = liftT $ Left $ SanityError p ("can not print " +++ toString t)
 299                     _ = pure f) >>= \newF->
 300                 pure (compose s2 s1, returnType, FunExpr p newF args_ fs))
 301
 302     IntExpr _ _ = pure $ (zero, IntType, e)
 303     BoolExpr _ _ = pure $ (zero, BoolType, e)
 304     CharExpr _ _ = pure $ (zero, CharType, e)
 305
 306 foldFieldSelectors :: Type FieldSelector -> Typing Type
 307 foldFieldSelectors (ListType t) (FieldHd) = pure t
 308 foldFieldSelectors t=:(ListType _) (FieldTl) = pure t
 309 foldFieldSelectors (TupleType (t1, _)) (FieldFst) = pure t1
 310 foldFieldSelectors (TupleType (_, t2)) (FieldSnd) = pure t2
 311 foldFieldSelectors t fs = liftT $ Left $ FieldSelectorError zero t fs
 312
 313 op2Type :: Op2 -> Typing Type
 314 op2Type op
 315 | elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 316   = pure (IntType ->> IntType ->> IntType)
 317 | elem op [BiEquals, BiUnEqual]
 318   = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 319 | elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 320   = pure (IntType ->> IntType ->> BoolType)
 321 | elem op [BiAnd, BiOr]
 322   = pure (BoolType ->> BoolType ->> BoolType)
 323 | op == BiCons
 324   = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)
 325
 326 op1Type :: Op1 -> Typing Type
 327 op1Type UnNegation = pure $ (BoolType ->> BoolType)
 328 op1Type UnMinus = pure $ (IntType ->> IntType)
 329
 330 ////----- Inference for Statements -----
 331 applySubst :: Substitution -> Typing Gamma
 332 applySubst s = changeGamma (subst s)
 333
 334 instance infer Stmt where
 335  infer s = case s of
 336     IfStmt e th el =
 337         infer e >>= \(s1, et, e_)->
 338         lift (unify et BoolType) >>= \s2 ->
 339         applySubst (compose s2 s1) >>|
 340         infer th >>= \(s3, tht, th_)->
 341         applySubst s3 >>|
 342         infer el >>= \(s4, elt, el_)->
 343         applySubst s4 >>|
 344         lift (unify tht elt) >>= \s5->
 345         let sub = compose s5 $ compose s4 $ compose s3 $ compose s2 s1 in
 346         pure (sub, subst s5 tht, IfStmt e_ th_ el_)
 347
 348     WhileStmt e wh =
 349         infer e >>= \(s1, et, e_)->
 350         lift (unify et BoolType) >>= \s2 ->
 351         applySubst (compose s2 s1) >>|
 352         infer wh >>= \(s3, wht, wh_)->
 353         pure (compose s3 $ compose s2 s1, subst s3 wht, WhileStmt e_ wh_)
 354
 355     AssStmt vd=:(VarDef k fs) e =
 356         lookup k >>= \expected ->
 357         infer e >>= \(s1, given, e_)->
 358         foldM reverseFs given (reverse fs) >>= \varType->
 359         lift (unify expected varType) >>= \s2->
 360         let s = compose s2 s1 in
 361         applySubst s >>|
 362         changeGamma (extend k (Forall [] (subst s varType))) >>|
 363         pure (s, VoidType, AssStmt vd e_)
 364
 365     FunStmt f args fs =
 366         lookup f >>= \expected ->
 367         let accST = (\(s,ts,es) e->infer e >>= \(s_,et,e_)-> pure (compose s_ s,ts++[et],es++[e_])) in
 368         foldM accST (zero,[],[]) args >>= \(s1, argTs, args_)->
 369         fresh >>= \tv->
 370         let given = foldr (->>) tv argTs in
 371         lift (unify expected given) >>= \s2->
 372         let fReturnType = subst s2 tv in
 373         foldM foldFieldSelectors fReturnType fs >>= \returnType ->
 374         (case f of
 375             "print" = case head argTs of
 376                 IntType = pure "1printint"
 377                 CharType = pure "1printchar"
 378                 BoolType = pure "1printbool"
 379                 ListType (CharType) = pure "1printstr"
 380                 t = liftT $ Left $ SanityError zero ("can not print " +++ toString t)
 381             _ = pure f) >>= \newF->
 382         pure (compose s2 s1, VoidType, FunStmt newF args_ fs)
 383
 384     ReturnStmt Nothing = pure (zero, VoidType, s)
 385     ReturnStmt (Just e) = infer e >>= \(sub, t, _)-> pure (sub, t, s)
 386
 387 reverseFs :: Type FieldSelector -> Typing Type
 388 reverseFs t FieldHd = pure $ ListType t
 389 reverseFs t FieldTl = pure $ ListType t
 390 reverseFs t FieldFst = fresh >>= \tv -> pure $ TupleType (t, tv)
 391 reverseFs t FieldSnd = fresh >>= \tv -> pure $ TupleType (tv, t)
 392
 393 //The type of a list of statements is either an encountered
 394 //return, or VoidType
 395 instance infer [a] | infer a where
 396     infer []        = pure (zero, VoidType, [])
 397     infer [stmt:ss] =
 398         infer stmt >>= \(s1, t1, s_) ->
 399         applySubst s1 >>|
 400         infer ss >>= \(s2, t2, ss_) ->
 401         applySubst s2 >>|
 402         case t1 of
 403             VoidType = pure (compose s2 s1, t2, [s_:ss_])
 404             _ = case t2 of
 405                 VoidType = pure (compose s2 s1, t1, [s_:ss_])
 406                 _ = lift (unify t1 t2) >>= \s3 ->
 407                     pure (compose s3 $ compose s2 s1, t1, [s_:ss_])
 408
 409 //the type class inferes the type of an AST element (VarDecl or FunDecl)
 410 //and adds it to the AST element
 411 class type a :: a -> Typing (Substitution, a)
 412
 413 instance type VarDecl where
 414     type (VarDecl p expected k e) =
 415         infer e >>= \(s1, given, e_) ->
 416         applySubst s1 >>|
 417         case expected of
 418             Nothing = pure zero
 419             Just expected_ = lift (unify expected_ given)
 420         >>= \s2->
 421         applySubst s2 >>|
 422         let vtype = subst (compose s2 s1) given in
 423         generalize vtype >>= \t ->
 424         changeGamma (extend k t) >>|
 425         pure (compose s2 s1, VarDecl p (Just vtype) k e_)
 426
 427 instance type FunDecl where
 428     type fd=:(FunDecl p f args expected vds stmts) =
 429         //if (f=="main") (abort (toString fd)) (pure ()) >>|
 430         gamma >>= \outerScope-> //functions are infered in their own scopde
 431         introduce f >>|
 432         mapM introduce args >>= \argTs->
 433         type vds >>= \(s1, tVds)->
 434         applySubst s1 >>|
 435         infer stmts >>= \(s2, result, stmts_)->
 436         applySubst s1 >>|
 437         let argTs_ = map (subst $ compose s2 s1) argTs in
 438         let given = foldr (->>) result argTs_ in
 439         (case expected of
 440             Nothing = pure zero
 441             Just (FuncType expected_) = lift (unify expected_ given)
 442             Just expected_ = lift (unify expected_ given)
 443         ) >>= \s3 ->
 444         let ftype = subst (compose s3 $ compose s2 s1) given in
 445         (case ftype of
 446             _ ->> _ = pure ftype
 447             _       = pure $ FuncType ftype
 448         ) >>= \ftype_->
 449         generalize ftype_ >>= \t->
 450         putGamma outerScope >>|
 451         changeGamma (extend f t) >>|
 452         pure (compose s3 $ compose s2 s1, FunDecl p f args (Just ftype_) tVds stmts_)
 453
 454 instance type [a] | type a where
 455     type []     = pure (zero, [])
 456     type [v:vs] =
 457         type v >>= \(s1, v_)->
 458         applySubst s1 >>|
 459         type vs >>= \(s2, vs_)->
 460         applySubst (compose s2 s1) >>|
 461         pure (compose s2 s1, [v_:vs_])
 462
 463 introduce :: String -> Typing Type
 464 introduce k =
 465     fresh >>= \tv ->
 466     changeGamma (extend k (Forall [] tv)) >>|
 467     pure tv
 468
 469 instance toString Scheme where
 470     toString (Forall x t) =
 471         concat ["Forall ": intersperse "," x] +++ concat [". ", toString t];
 472
 473 instance toString Gamma where
 474     toString mp =
 475         concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 476
 477 instance toString Substitution where
 478     toString subs =
 479         concat [concat [k, ": ", toString t, "\n"]\\(k, t)<-'Map'.toList subs]
 480
 481 instance toString SemError where
 482     toString (SanityError p e) = concat [toString p,
 483         "SemError: SanityError: ", e]
 484     toString (ParseError p s) = concat [toString p,
 485         "ParseError: ", s]
 486     toString (UnifyError p t1 t2) = concat [toString p,
 487         "Can not unify types, expected|given:\n", toString t1,
 488         "\n", toString t2]
 489     toString (InfiniteTypeError p t) = concat [toString p,
 490         "Infinite type: ", toString t]
 491     toString (FieldSelectorError p t fs) = concat [toString p,
 492         "Can not run fieldselector '", toString fs, "' on type: ",
 493         toString t]
 494     toString (OperatorError p op t) = concat [toString p,
 495         "Operator error, operator '", toString op, "' can not be",
 496         "used on type: ", toString t]
 497     toString (UndeclaredVariableError p k) = concat [toString p,
 498         "Undeclared identifier: ", k]
 499     toString (ArgumentMisMatchError p str) = concat [toString p,
 500         "Argument mismatch: ", str]
 501     toString (Error e) = concat ["Unknown error during semantical",
 502         "analysis: ", e]
 503
 504 instance toString (Maybe a) | toString a where
 505     toString Nothing = "Nothing"
 506     toString (Just e) = concat ["Just ", toString e]
 507
 508 instance MonadTrans (StateT (Gamma, [TVar])) where
 509     liftT m = StateT \s-> m >>= \a-> return (a, s)
 510
 511 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 512 Mapmap _ 'Map'.Tip = 'Map'.Tip
 513 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 514                                         (Mapmap f ml)
 515                                         (Mapmap f mr)