Commit c3ad38d7 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Rearrange the typechecking of arrows, especially arrow "forms"

The typechecking of arrow forms (in GHC 7.6) is known to be bogus, as
described in Trac #5609, because it marches down tuple types that may
not yet be fully worked out, depending on when constraint solving
happens.  Moreover, coercions are generated and simply discarded.  The
fact that it works at all is a miracle.

This refactoring is based on a conversation with Ross, where we
rearranged the typing of the argument stack, so that the arrows
have the form
   a (env, (arg1, (arg2, ...(argn, ())))) res
rather than
   a (arg1, (arg2, ...(argn, env))) res
as it was before.

This is vastly simpler to typecheck; just look at the beautiful,
simple type checking of arrow forms now!

We need a new HsCmdCast to capture the coercions generated from
the argument stack.

This leaves us in a better position to tackle the open arrow tickets
 * Trac #5777 still fails.  (I was hoping this patch would cure it.)
 * Trac #5609 is too complicated for me to grok.  Ross?
 * Trac #344
 * Trac #5333
parent 3ea331b7
......@@ -803,6 +803,9 @@ addTickHsCmd (HsCmdArrForm e fix cmdtop) =
(return fix)
(mapM (liftL (addTickHsCmdTop)) cmdtop)
addTickHsCmd (HsCmdCast co cmd)
= liftM2 HsCmdCast (return co) (addTickHsCmd cmd)
-- Others should never happen in a command context.
--addTickHsCmd e = pprPanic "addTickHsCmd" (ppr e)
......
This diff is collapsed.
......@@ -689,6 +689,12 @@ data HsCmd id
| HsCmdDo [CmdLStmt id]
PostTcType -- Type of the whole expression
| HsCmdCast TcCoercion -- A simpler version of HsWrap in HsExpr
(HsCmd id) -- If cmd :: arg1 --> res
-- co :: arg1 ~ arg2
-- Then (HsCmdCast co cmd) :: arg2 --> res
deriving (Data, Typeable)
data HsArrAppType = HsHigherOrderApp | HsFirstOrderApp
......@@ -705,7 +711,7 @@ type LHsCmdTop id = Located (HsCmdTop id)
data HsCmdTop id
= HsCmdTop (LHsCmd id)
[PostTcType] -- types of inputs on the command's stack
PostTcType -- Nested tuple of inputs on the command's stack
PostTcType -- return type of the command
(CmdSyntaxTable id) -- See Note [CmdSyntaxTable]
deriving (Data, Typeable)
......@@ -772,8 +778,9 @@ ppr_cmd (HsCmdLet binds cmd)
= sep [hang (ptext (sLit "let")) 2 (pprBinds binds),
hang (ptext (sLit "in")) 2 (ppr cmd)]
ppr_cmd (HsCmdDo stmts _) = pprDo ArrowExpr stmts
ppr_cmd (HsCmdDo stmts _) = pprDo ArrowExpr stmts
ppr_cmd (HsCmdCast co cmd) = sep [ ppr_cmd cmd
, ptext (sLit "|>") <+> ppr co ]
ppr_cmd (HsCmdArrApp arrow arg _ HsFirstOrderApp True)
= hsep [ppr_lexpr arrow, ptext (sLit "-<"), ppr_lexpr arg]
......
%
% (c) The University of Glasgow, 1992-2006
%
......@@ -29,7 +28,7 @@ module HsUtils(
mkHsWrap, mkLHsWrap, mkHsWrapCo, mkLHsWrapCo,
coToHsWrapper, mkHsDictLet, mkHsLams,
mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo,
mkLHsPar,
mkLHsPar, mkHsCmdCast,
nlHsTyApp, nlHsVar, nlHsLit, nlHsApp, nlHsApps, nlHsIntLit, nlHsVarApps,
nlHsDo, nlHsOpApp, nlHsLam, nlHsPar, nlHsIf, nlHsCase, nlList,
......@@ -394,6 +393,10 @@ mkLHsWrapCo :: TcCoercion -> LHsExpr id -> LHsExpr id
mkLHsWrapCo co (L loc e) | isTcReflCo co = L loc e
| otherwise = L loc (mkHsWrap (WpCast co) e)
mkHsCmdCast :: TcCoercion -> HsCmd id -> HsCmd id
mkHsCmdCast co cmd | isTcReflCo co = cmd
| otherwise = HsCmdCast co cmd
coToHsWrapper :: TcCoercion -> HsWrapper
coToHsWrapper co | isTcReflCo co = idHsWrapper
| otherwise = WpCast co
......
......@@ -1464,7 +1464,7 @@ exp10 :: { LHsExpr RdrName }
| 'proc' aexp '->' exp
{% checkPattern empty $2 >>= \ p ->
checkCommand $4 >>= \ cmd ->
return (LL $ HsProc p (LL $ HsCmdTop cmd []
return (LL $ HsProc p (LL $ HsCmdTop cmd placeHolderType
placeHolderType undefined)) }
-- TODO: is LL right here?
......@@ -1559,7 +1559,7 @@ cmdargs :: { [LHsCmdTop RdrName] }
acmd :: { LHsCmdTop RdrName }
: aexp2 {% checkCommand $1 >>= \ cmd ->
return (L1 $ HsCmdTop cmd [] placeHolderType undefined) }
return (L1 $ HsCmdTop cmd placeHolderType placeHolderType undefined) }
cvtopbody :: { [LHsDecl RdrName] }
: '{' cvtopdecls0 '}' { $2 }
......
......@@ -872,8 +872,8 @@ checkCmd _ (OpApp eLeft op fixity eRight) = do
-- OpApp becomes a HsCmdArrForm with a (Just fixity) in it
c1 <- checkCommand eLeft
c2 <- checkCommand eRight
let arg1 = L (getLoc c1) $ HsCmdTop c1 [] placeHolderType []
arg2 = L (getLoc c2) $ HsCmdTop c2 [] placeHolderType []
let arg1 = L (getLoc c1) $ HsCmdTop c1 placeHolderType placeHolderType []
arg2 = L (getLoc c2) $ HsCmdTop c2 placeHolderType placeHolderType []
return $ HsCmdArrForm op (Just fixity) [arg1, arg2]
checkCmd l e = cmdFail l e
......
......@@ -433,7 +433,7 @@ rnCmdTop = wrapLocFstM rnCmdTop'
-- Generate the rebindable syntax for the monad
; (cmd_names', cmd_fvs) <- lookupSyntaxNames cmd_names
; return (HsCmdTop cmd' [] placeHolderType (cmd_names `zip` cmd_names'),
; return (HsCmdTop cmd' placeHolderType placeHolderType (cmd_names `zip` cmd_names'),
fvCmd `plusFV` cmd_fvs) }
rnLCmd :: LHsCmd RdrName -> RnM (LHsCmd Name, FreeVars)
......@@ -511,6 +511,7 @@ rnCmd (HsCmdDo stmts _)
= do { ((stmts', _), fvs) <- rnStmts ArrowExpr rnLCmd stmts (\ _ -> return ((), emptyFVs))
; return ( HsCmdDo stmts' placeHolderType, fvs ) }
rnCmd cmd@(HsCmdCast {}) = pprPanic "rnCmd" (ppr cmd)
---------------------------------------------------
type CmdNeeds = FreeVars -- Only inhabitants are
......@@ -527,6 +528,7 @@ methodNamesCmd (HsCmdArrApp _arrow _arg _ HsFirstOrderApp _rtl)
methodNamesCmd (HsCmdArrApp _arrow _arg _ HsHigherOrderApp _rtl)
= unitFV appAName
methodNamesCmd (HsCmdArrForm {}) = emptyFVs
methodNamesCmd (HsCmdCast _ cmd) = methodNamesCmd cmd
methodNamesCmd (HsCmdPar c) = methodNamesLCmd c
......
......@@ -679,7 +679,7 @@ mkOpFormRn a1@(L loc (HsCmdTop (L _ (HsCmdArrForm op1 (Just fix1) [a11,a12])) _
| associate_right
= do new_c <- mkOpFormRn a12 op2 fix2 a2
return (HsCmdArrForm op1 (Just fix1)
[a11, L loc (HsCmdTop (L loc new_c) [] placeHolderType [])])
[a11, L loc (HsCmdTop (L loc new_c) placeHolderType placeHolderType [])])
-- TODO: locs are wrong
where
(nofix_error, associate_right) = compareFixity fix1 fix2
......
This diff is collapsed.
......@@ -730,6 +730,10 @@ zonkCmd :: ZonkEnv -> HsCmd TcId -> TcM (HsCmd Id)
zonkLCmd env cmd = wrapLocM (zonkCmd env) cmd
zonkCmd env (HsCmdCast co cmd)
= do { co' <- zonkTcLCoToLCo env co
; cmd' <- zonkCmd env cmd
; return (HsCmdCast co' cmd') }
zonkCmd env (HsCmdArrApp e1 e2 ty ho rl)
= zonkLExpr env e1 `thenM` \ new_e1 ->
zonkLExpr env e2 `thenM` \ new_e2 ->
......@@ -786,7 +790,7 @@ zonkCmdTop env cmd = wrapLocM (zonk_cmd_top env) cmd
zonk_cmd_top :: ZonkEnv -> HsCmdTop TcId -> TcM (HsCmdTop Id)
zonk_cmd_top env (HsCmdTop cmd stack_tys ty ids)
= zonkLCmd env cmd `thenM` \ new_cmd ->
zonkTcTypeToTypes env stack_tys `thenM` \ new_stack_tys ->
zonkTcTypeToType env stack_tys `thenM` \ new_stack_tys ->
zonkTcTypeToType env ty `thenM` \ new_ty ->
mapSndM (zonkExpr env) ids `thenM` \ new_ids ->
returnM (HsCmdTop new_cmd new_stack_tys new_ty new_ids)
......
......@@ -8226,7 +8226,7 @@ Thus combinators that produce arrows from arrows
may also be used to build commands from commands.
For example, the <literal>ArrowPlus</literal> class includes a combinator
<programlisting>
ArrowPlus a => (&lt;+>) :: a e c -> a e c -> a e c
ArrowPlus a => (&lt;+>) :: a b c -> a b c -> a b c
</programlisting>
so we can use it to build commands:
<programlisting>
......@@ -8256,18 +8256,24 @@ expr' = (proc x -> returnA -&lt; x)
y &lt;- term -&lt; ()
expr' -&lt; x - y)
</programlisting>
We are actually using <literal>&lt;+></literal> here with the more specific type
<programlisting>
ArrowPlus a => (&lt;+>) :: a (e,()) c -> a (e,()) c -> a (e,()) c
</programlisting>
It is essential that this operator be polymorphic in <literal>e</literal>
(representing the environment input to the command
and thence to its subcommands)
and satisfy the corresponding naturality property
<screen>
arr k >>> (f &lt;+> g) = (arr k >>> f) &lt;+> (arr k >>> g)
arr (first k) >>> (f &lt;+> g) = (arr (first k) >>> f) &lt;+> (arr (first k) >>> g)
</screen>
at least for strict <literal>k</literal>.
(This should be automatic if you're not using <function>seq</function>.)
This ensures that environments seen by the subcommands are environments
of the whole command,
and also allows the translation to safely trim these environments.
(The second component of the input pairs can contain unnamed input values,
as described in the next section.)
The operator must also not use any variable defined within the current
arrow abstraction.
</para>
......@@ -8275,7 +8281,7 @@ arrow abstraction.
<para>
We could define our own operator
<programlisting>
untilA :: ArrowChoice a => a e () -> a e Bool -> a e ()
untilA :: ArrowChoice a => a (e,s) () -> a (e,s) Bool -> a (e,s) ()
untilA body cond = proc x ->
b &lt;- cond -&lt; x
if b then returnA -&lt; ()
......@@ -8305,7 +8311,7 @@ the operator that attaches an exception handler will wish to pass the
exception that occurred to the handler.
Such an operator might have a type
<screen>
handleA :: ... => a e c -> a (e,Ex) c -> a e c
handleA :: ... => a (e,s) c -> a (e,(Ex,s)) c -> a (e,s) c
</screen>
where <literal>Ex</literal> is the type of exceptions handled.
You could then use this with arrow notation by writing a command
......@@ -8320,22 +8326,24 @@ Though the syntax here looks like a functional lambda,
we are talking about commands, and something different is going on.
The input to the arrow represented by a command consists of values for
the free local variables in the command, plus a stack of anonymous values.
In all the prior examples, this stack was empty.
In all the prior examples, we made no assumptions about this stack.
In the second argument to <function>handleA</function>,
this stack consists of one value, the value of the exception.
the value of the exception has been added to the stack input to the handler.
The command form of lambda merely gives this value a name.
</para>
<para>
More concretely,
the values on the stack are paired to the right of the environment.
the input to a command consists of a pair of an environment and a stack.
Each value on the stack is paired with the remainder of the stack,
with an empty stack being <literal>()</literal>.
So operators like <function>handleA</function> that pass
extra inputs to their subcommands can be designed for use with the notation
by pairing the values with the environment in this way.
by placing the values on the stack paired with the environment in this way.
More precisely, the type of each argument of the operator (and its result)
should have the form
<screen>
a (...(e,t1), ... tn) t
a (e, (t1, ... (tn, ())...)) t
</screen>
where <replaceable>e</replaceable> is a polymorphic variable
(representing the environment)
......@@ -8347,9 +8355,9 @@ The polymorphic variable <replaceable>e</replaceable> must not occur in
However the arrows involved need not be the same.
Here are some more examples of suitable operators:
<screen>
bracketA :: ... => a e b -> a (e,b) c -> a (e,c) d -> a e d
runReader :: ... => a e c -> a' (e,State) c
runState :: ... => a e c -> a' (e,State) (c,State)
bracketA :: ... => a (e,s) b -> a (e,(b,s)) c -> a (e,(c,s)) d -> a (e,s) d
runReader :: ... => a (e,s) c -> a' (e,(State,s)) c
runState :: ... => a (e,s) c -> a' (e,(State,s)) (c,State)
</screen>
We can supply the extra input required by commands built with the last two
by applying them to ordinary expressions, as in
......@@ -8371,16 +8379,16 @@ are the core of the notation; everything else can be built using them,
though the results would be somewhat clumsy.
For example, we could simulate <literal>do</literal>-notation by defining
<programlisting>
bind :: Arrow a => a e b -> a (e,b) c -> a e c
bind :: Arrow a => a (e,s) b -> a (e,(b,s)) c -> a (e,s) c
u `bind` f = returnA &amp;&amp;&amp; u >>> f
bind_ :: Arrow a => a e b -> a e c -> a e c
bind_ :: Arrow a => a (e,s) b -> a (e,s) c -> a (e,s) c
u `bind_` f = u `bind` (arr fst >>> f)
</programlisting>
We could simulate <literal>if</literal> by defining
<programlisting>
cond :: ArrowChoice a => a e b -> a e b -> a (e,Bool) b
cond f g = arr (\ (e,b) -> if b then Left e else Right e) >>> f ||| g
cond :: ArrowChoice a => a (e,s) b -> a (e,s) b -> a (e,(Bool,s)) b
cond f g = arr (\ (e,(b,s)) -> if b then Left (e,s) else Right (e,s)) >>> f ||| g
</programlisting>
</para>
......@@ -8405,6 +8413,14 @@ a new <literal>form</literal> keyword.
</para>
</listitem>
<listitem>
<para>In the paper and the previous implementation,
values on the stack were paired to the right of the environment
in a single argument,
but now the environment and stack are separate arguments.
</para>
</listitem>
</itemizedlist>
</sect2>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment