
\section{Effect and Closure typing}
Along with region typing, Disciple includes effect and closure typing \CITE. We use effect typing to reason about side-effects in a more fine-grained way than is possible in Haskell with its IO and ST monads. Effect information is used to track when it is safe to use lazy evaluation, which we will discuss in \REF. Effect information is also used by the optimiser during compilation \CITE. Closure information is used to control generalisation during type inference, and to mitigate the potential unsoundness due to destructive update which the ML family of languages typically solve via the value restriction \cite{garrigue:relaxing}. We will discuss other uses of closure information in \REF.

When all information is included, the type of @updateInt@ from the previous section is:

\begin{code}
 updateInt :: forall %r1 %r2 !e1 $c1. Mutable %r1
           => Int %r1 -> Int %r2 -(!e1 $c1)> ()
           :- !e1 :> !Write %r1 + !Read %r2
           ,  $c1 :> $Clo (Int %r1)
\end{code}
Once again, although this is the full, gory type for @updateInt@, the programmer usually doesn't need to concern themselves with such signatures. Disciple supports full type inference, and common patterns in signatures are handled by defaulting rules. We'll discuss this further in \REF.

In the type for @updateInt@, the variables @!e1@ and @$c1@ are effect and closure variables respectively. The symbol @!@ is both the namespace qualifier for effect variables, and kind of effect types. We use @!@ as a mnemonic for ``something's happening!''. Likewise @$@ is is the namespace qualifier and kind of closure types. When we think about @$@ we think about ``expansion'', like in a Makefile or Perl program.\footnote{but more pleasingly}. The full grammar for type expressions is given in \REF. In this paper we treat the syntax @TYPE :- CONSTRAINT@ as sugar for bounded quantification, with the desugaring rules given in \REF. This is sufficient for top-level type signatures, though during type inference we allow constraints to be given separately from quantifiers, which is discussed in \CITE. 

In the type of @updateInt@, the effect and closure constraints give the effect and closure of the rightmost function arrow. We have written @!e1@ and @$c1@ inline with the function constructor @->@. Our function constructor has four parameters, the argument type, the return type, its effect and closure. This use of the infix function constructor desugars to @(->) (Int %r2) () !e1 $c1@. This gives our function constructor the following kind: 
\begin{code}
        (->) :: * -> * -> ! -> $ -> *
\end{code}

Like the function arrow @(->)@, the constructor @!Read@ is ``baked in'' to our system. This constructor takes a region and produces an effect, and hence has the kind @!Read :: % -> !@. The constructor @$Clo@ takes a type and produces a closure, so it has kind @$Clo :: * -> $@. The kinds of our baked in type constructors are shown in \REF.

Returning to the type of @updateInt@, the effect term \\ @!Write %r1 + !Read %r2@ reveals that this function reads its second argument and writes to its first. Note there is no temporal ordering implied by the way these effects are written. Operationally, @updateInt@ must read its source before writing to its destination, but this information is not encoded by the type. Effects types form an upwards semi-lattice ordered by set inclusion, with @!0@ being the least element (purity) and @+@ behaving similarly to set union. In prior work \CITE we have written @!0@ and @+@ as $\bot$ and $\lor$. Note that with @!Read@ and @!Write@, the @!@ symbols are namespace qualifiers. This means that @!Read@ and @Read@ are distinct names, with distinct meanings.

The constructor @$Clo@ takes a value type and produces a closure type, thus has kind @$Clo :: * -> $@. In the type of @updateInt@ the term @$Clo (Int %r1)@ reveals that this function references a value of type @Int %r1@ from its environment. This happens if @updateInt@ is partially applied. Closure types have a similar lattice structure as effects, with @$0@ being the least element (emptiness) and we overload @+@ to also sum closures.  

We define @*0@ as @%0@ as value and region types respectively, though we only permit them in the constraint attached to a @forall@. This is a syntactic convenience, and we could eliminate the need for @*0@ and @%0@ by defining an unbounded version of @forall@ that doesn't require a constraint. There is no corresponding lattice structure for value and region types, and our @+@ type operator applies to effects and closures only. 

In Figure \ref{fig:TypeExpressions} we have written @...@ to indicate that new data types can be defined by the user using @data@ declarations. The constructors @!Console@ and @!File@ are representative ``global'' effects that indicate an interaction with the outside world. These global effects are defined in source programs, but see \CITE for the syntax. We use @CLS@ to represent a user defined type class constructor, such as @Show@ or @Eq@. These are defined with @class@ declarations similarly to Haskell, which we will discuss in the next section.  

\begin{figure}
\begin{small}
\begin{code}
KIND  ::= *         -- kind of value types
       |  %         -- kind of region types
       |  !         -- kind of effect types
       |  $         -- kind of closure types

VAR   ::= v         -- type variable of arbitrary kind
       |  a | b | c -- value   type variables
       |  %r        -- region  type variable
       |  !e        -- effect  type variable
       |  $c        -- closure type variable

TYPE  ::= forall (v :> BTYPE). PTYPE -- bounded quant.
       |  PTYPE 

PTYPE ::= PRED => PTYPE             -- type class predicate
       |  BTYPE

BTYPE ::= VAR                       -- variable
       |  CTOR                      -- type constructor
       |  BTYPE BTYPE               -- type application
       |  BTYPE + BTYPE             -- type summation
       |  KIND 0                    -- least element

CTOR  ::= Int       | Char          -- data type ctors
       |  List      | Maybe  | ...
       |  !Read     | !Write        -- effect type ctors
       |  !DeepRead | !DeepWrite
       |  !Console  | !File  | ...
       |  $Clo                      -- closure ctor

PRED  ::= CLS TYPE                  -- value type class
       |  Lazy  %r  | Direct  %r    -- discussed in S...
       |  Const %r  | Mutable %r    -- discussed in S...
       |  Pure TYPE | Empty TYPE    -- discussed in S...
       |  DeepConst   TYPE          -- discussed in S...
       |  DeepMutable TYPE          -- discussed in S...
       |  HeadLazy    TYPE          -- discussed in S...
       |  Shape       TYPE TYPE     -- discussed in S...
\end{code}
\end{small}
\caption{Type expressions}
\label{fig:TypeExpressions}
\end{figure}

% -----------------------------------------------------------------------------
\begin{figure}
\begin{small}
\begin{code}
    a -(!e $c)> b     ==> (->) a b !e $c

    forall  a. TYPE   ==> forall ( a :> *0). TYPE
    forall %r. TYPE   ==> forall (%r :> %0). TYPE
    forall !e. TYPE   ==> forall (!e :> !0). TYPE
    forall $c. TYPE   ==> forall ($c :> $0). TYPE

    forall (v1 :> TYPE1) (v2 :> TYPE2). TYPE3
==> forall (v1 :> TYPE1). forall (v2 :> TYPE2). TYPE3

    forall v1. TYPE1 :- v1 :> TYPE2
==> forall (v1 :> TYPE2). TYPE1

    TODO: add rule for ',' in constraints.
    TODO: discuss how to read a -> b with no effect
          or closure variables.

\end{code}
\end{small}
\caption{Desugaring type expressions}
\label{fig:DesugaringTypeExpressions}
\end{figure}

% -----------------------------------------------------------------------------
\begin{figure}
\begin{small}
\begin{code}
(->)      :: * -> * -> ! -> $ -> *
Int       :: % -> *
Char      :: % -> *
List      :: % -> * -> *
Maybe     :: % -> * -> *
!Read     :: % -> !        !Write     :: % -> !
!DeepRead :: * -> !        !DeepWrite :: * -> !
$Clo      :: * -> $
\end{code}
\end{small}
\caption{Kinds of baked in type constructors}
\label{fig:BakedInConstructors}
\end{figure}






% \subsection{Higher order functions and closure trimming}
% \begin{small}
% \begin{code}
% zipWith_ 
%   :: forall a b c %r1 %r2
%   .  Mutable %r1 %r2
%   => (a -(!e1)> b -(!e2)> ()) 
%      -> List %r1 a -($c3)> List %r2 b -(!e4 $c4)> ()
%   :- $c3 = $Clo (a -(!e1)> b -(!e2)> ())
%   ,  $c4 = $Clo (a -(!e1)> b -(!e2)> ()) + $Clo (List %r1 a)
%   ,  !e4 = !e1 + !e2 + !Read %r1 + !Read %r2
% \end{code}
% \end{small}


