
% -------------------------------------------------------------------------------------------------
\section{Shape Constraints}

The problem with method types being over constrained occurs any time we wish to produce a value of some type from an old one, while requiring the \emph{shape} of those types to be identical. The simplest operation in this category is @copy@, which physically copies its argument, producing new objects in the store. 

Reusing the example form the previous section, here is the type of the primitive copy operator that works on integers:
\begin{code}
 copyInt :: forall %r1 %r2 !e1
         .  Int %r1 -(!e1)> Int %r2
         :- !e1 :> !Read %r1
\end{code}
Now for the version that works on lists of integers:

\begin{code}
 copyListInt 
  :: forall %r1 %r2 %r3 %r4 !e1
  .  List %r1 (Int %r2) -(!e1)> List %r3 (Int %r4)
  :- !e1 :> !Read %r1 + !Read %r2

 copyListInt xx
  = case xx of
     Nil       -> Nil
     Cons x xs -> Cons (copyInt x) 
                       (copyListInt xs)
\end{code}

The fact that these functions produce new objects in the store, instead of just returning the old ones, is revealed in their types. The type of @copyInt@ says it accepts a value in region @%r1@, and produces one into region @%r2@, for any @%r2@ we like. 

As @copyInt@ and @copyListInt@ perform similar operations, we would like to define a type class that abstracts them both. In general, a copying function could read any region in its parameter, hence we use the @!DeepRead@ effect from the previous section and try something like:

\begin{code}
  class Copy a where
    copy :: forall !e. a -(!e)> a
         :- !e :> !DeepRead a
\end{code}

Unfortunately, this signature for @copy@ does not indicate that the returned object should be fresh. Our @copyInt@ function produces a freshly allocated object, but the @Int@ instance of this type class would have type:

\begin{code}
 copy[Int] :: forall %r1 !e. Int %r1 -(!e)> Int %r1
           :- !e :> !Read %r1
\end{code}

This would prevent us from using our overloaded @copy@ function to make local, mutable copies of constant integers. This is similar to the problem we had with the @Update@ class from the previous section. On the other hand, the following signature is too weak:

\begin{code}
  class Copy a where
    copy :: forall b !e. a -(!e)> b
         :- !e :> !DeepRead a
\end{code}

If the argument of @copy@ is an integer, then we expect the return value to also be an integer. What we need is for the argument and return types of @copy@ to have the same overall shape, while allowing their contained region variables (and effect and closure information) to vary. We enforce this with the (predictably named) @Shape@ constraint:

\begin{code}
  class Copy a where
    copy :: forall b !e. Shape a b => a -(!e)> b
         :- !e :> !DeepRead a
\end{code}

The constraint @Shape@ can be viewed as a functional dependency \cite{jones:functional-dependencies} between the two types @a@ and @b@. The dependency is bi-directional, so if @a@ is an @Int@ then @b@ must also be an @Int@, and if @b@ is an @Int@ then so must @a@. As with @DeepMutable@ we also automatically generate the appropriate instances from the type class definition. As before, we don't need to constrain type variables that only appear in function types in the data definition, but we'll cover that in the next section.

\begin{code}
  instance Shape (Int %r1) (Int %r2) 

  instance Shape a b 
        => Shape (List %r1 a) (List %r2 b) 
  ...
\end{code}

As mentioned earlier, the @Shape@ constraint also solves the problem we had when defining the @Update@ class. Here is the final version:

\begin{code}
 class Update a where
   (:=) :: forall b !e1. Shape a b => DeepMutable a
        => a -> b -(!e1 $c1)> ()
        :- !e1 :> !DeepWrite a + !DeepRead b
        ,  $c1 :> $Clo a
\end{code}

With this type, we can now use @(:=)@ to use a the value of a constant object to update the value of a mutable one, as the @Shape@ constraint allows the source and destination values to be in different regions. As a final example of the utility of @Shape@, we present our version of the venerable type class @Eq@.
\begin{code}
  class Eq a where
    (==) :: forall b %r1 !e1 $c1. Shape a b
         => a -> b -(!e1 $c1)> Bool %r1
         :- !e1 :> !DeepRead a + !DeepRead b
         ,  $c1 :> $Clo a
\end{code}

This says that instances of @(==)@ accept two arguments, and return a fresh boolean. Instances are permitted to read any region in their arguments and hold a reference to the first one when partially applied. We use the @Shape@ constraint because, once again, we don't require both arguments to have exactly the same type. Doing so would prevent is from, say, comparing the value of a @Mutable@ integer with that of a @Const@ one.


% -------------------------------------------------------------------------------------------------
\subsection{Shape Constraints and Rigid Variables}
In the examples from the previous section, note that when we added the shape constraint we also introduced a new variable (usually @b@) for the type of the second parameter of the constraint. As this variable is quantified locally in the type signature for the method, and does not appear in the head of the class definition (like @class Eq a where)@ we say that this variable is \emph{rigid} \CITE. Compare this with the example in Haskell:

\begin{code}
  class Foo a where
    foo :: forall b. a -> List b -> List b
\end{code}
An instance of this class is:
\begin{code}
  instance Foo Bool where
    foo x y = if x then tail y else reverse y
\end{code}
The locally quantified type variable @b@ is rigid because every instance of @foo@ must have a similarly general type. For example, the following non-instance is invalid:
\begin{code}
  instance Foo Char where
    foo x y = if x == 'a' then tail y else [x]
\end{code}
This non-instance tries to assign @foo@ the following type:
\begin{code}
  foo[Char] :: Char -> List Char -> List Char
\end{code}
This is strictly less general than the one in the class declaration, because we cannot apply it to lists whose elements do not have type @Char@.

Now, our @Copy@ type class declaration from the previous section also uses a rigid type variable. Here it is again:

\begin{code}
 class Copy a where
   copy :: forall b !e. Shape a b => a -(!e)> b
        :- !e :> !DeepRead a
\end{code}
Note the local @forall b@ quantifier. We have said that @copyInt@ is a valid instance of @copy@ because it produces a freshly allocated object. Recall that @copyInt@ has the following type:

\begin{code}
 copyInt :: forall %r1 %r2 !e1
         .  Int %r1 -(!e1)> Int %r2
         :- !e1 :> Read %r1
\end{code}
On the other hand, the following instance is \emph{not} valid.

\begin{code}
  instance Copy Char where
    copy x = x
\end{code}
Semantically, it is not valid because it does not actually copy its argument, though note that we can also see this fact in its type.

\begin{code}
  copy[Char] :: forall %r1. Char %r1 -> Char %r1
\end{code}
This situation is similar to the one with @foo[Char]@ because the signature of @copy[Char]@ is not sufficiently polymorphic to be used as an instance of @copy@.


% -----------------------------------------------------------------------------
\subsection{Determining the Instance Types}
We now discuss how to determine the required type of an instance function from the type class declaration. The subtle point is in dealing with @Shape@ constraints on rigid type variables. Here is the @Copy@ class declaration again, but for the sake of example we have added the outer quantifier for @a@.

\begin{code}
  forall a. class Copy a where
    copy :: forall b !e1. Shape a b
         => a -(!e1)> b
         :- !e1 :> !DeepRead a
\end{code}
Suppose that we wish to determine the required type of @copy[Int]@. To do this we instantiate the type class declaration with @Int r1@ where @r1@ is fresh. We can then re-generalise the declaration for @%r1@, to get a @forall %r1@ quantifier at top-level.

\begin{code}
  forall %r1. class Copy (Int %r1) where
    copy :: forall b !e1. Shape (Int %r1) b 
         => Int %r1 -(!e1)> b
         :- !e1 :> !DeepRead (Int %r1)
\end{code}
Reducing the @DeepRead@ effect and the @Shape@ constraint yields:

\begin{code}
  forall %r1. class Copy (Int %r1) where
    copy :: forall %r2 !e1
         .  Int %r1 -(!e1)> b
         :- !e1 :> !Read %r1
         ,  b   =  Int %r2
\end{code}
Reduction of the @Shape@ constraint has introduced the new type constraint ~@b = Int %r2@~ where @%r2@ is fresh. For the sake of example we have abused our syntax and written this constraint separately, instead of immediately substituting for @b@, to highlight the operation of @Shape@. We have also replaced @forall b@ with @forall %r2@. Every time the reduction of a @Shape@ constraint on a quantified type variable introduces a new region variable, we quantify the new variable instead of the old one. Substituting for @b@ completes the process.

\begin{code}
  forall %r1. class Copy (Int %r1) where
    copy :: forall %r2 !e1
         .  Int %r1 -(!e1)> Int %r2
         :- !e1 :> !Read %r1
\end{code}
Finally, when extracting the type of the @Int@ instance of @Copy@, we must remember to include the outer quantifier. 

\begin{code}
  copy :: forall %r1 %r2 !e1
       .  Int %r1 -(!e1)> Int %r2
       :- !e1 :> !Read %r1
\end{code}


% -----------------------------------------------------------------------------
\subsection{Faking it with Phantom Types}
A natural question whether our system can be encoded directly in Haskell. One technique for encoding information about the permitted use of a value (like constancy or mutability) is with so called \emph{phantom types} \cite{leijen:domain-specific-embedded-compilers, cheney:first-class-phantom-types} or GADTs \CITE. Ignoring effects and closure information, we could encode information about mutability as follows. The definitions of the associated functions are straightforward, so have been elided. 

\begin{code}
  data Mutable
  data Const

  data DInt m where
    MkDInt  :: IORef Int -> DInt m

  mkDInt    :: Int -> IO (DInt m)
  updateInt :: DInt Mutable -> DInt m -> IO ()
  copyInt   :: DInt m1      -> IO (DInt m2)
\end{code}

The intention is that the @m@ parameter of @DInt@ should only ever be instantiated with @Mutable@ or @Const@, but we cannot enforce this in Haskell. Continuing on, we could try to define our @Shape@ and @Copy@ classes as follows, using a functional dependency on @Shape@. Unfortunately, we get into trouble when we try to give the @Int@ instance for @Copy@.

\begin{code}
  class Shape a b | a -> b, b -> a

  class Copy a where
    copy :: forall b. Shape a b => a -> IO b

  instance (Shape (DInt m1) (DInt m2))
	
  instance Copy (DInt m) where    
    copy = copyInt                  -- BAD
\end{code}

\begin{flushleft}
The error message given by GHC 7.0.1 \CITE is as follows:
\end{flushleft}

\begin{code}
    Could not deduce (b ~ DInt m2) 
          from the context (Shape (DInt m) b)
      `b' is a rigid type variable bound by
          the type signature for `copy' at ...
\end{code}

This highlights the fact that our @Shape@ constraint is something above and beyond what is supported by current (extensions of) Haskell. In the error message, the term @(b ~ DInt m2)@ is an equality constraint, and \emph{rigid type variable} means one that is specified by a user signature in the source program \CITE (from type inference for GADTs 2006). Rigid type variables are related to the notion of \emph{skolem variables} from logic \CITE, meaning a specific but unknown member of some set. The error message then implies that the inferencer cannot prove that this ``specific but unknown member'' is the same as @DInt m2@, for some @m2@. The functional dependencies given in the definition of @Shape@ do not help in this respect.

For another way of looking at this, consider the type of the @copy@ method:
\begin{code}
   copy :: forall b. Shape a b => a -> IO b
\end{code}

With GHC, this type means ``for all types @b@, provided @b@ has the same shape as @a@, the function @copy@ takes an @a@ and produces a @b@''. In contrast, for Disciple the same type means ``for all types @b@ \emph{that have the same shape as @a@}, the function @copy@ takes an @a@ and produces a @b@''. In Disciple, the @Shape@ constraint provides a stronger link between the quantification of @a@ and @b@ than is present with the usual meaning of @forall@. 


