[http://trac.haskell.org/ddc/wiki/Language/Overview < Overview]
= Regions and the Class System =

== Regions ==
In short, two pieces of data are in different regions if they are never substituted for each other. This property, or lack thereof, is sometimes called ''aliasing''.

In the "extended" version of a type, data type constructors have a region annotation as their first argument, which indicates what region they're in. Due to type elaboration, we usually don't see the region annotations, but we can write them in signatures if we want to:

{{{
succ :: forall %r1 %r2. Int %r1 -> Int %r2
succ x = x + 1

sameInt :: forall %r1. Int %r1 -> Int %r1
sameInt x = x

pi :: Float %r1
pi = 3.1415926535
}}}

Region variables can be quantified with `forall` just like type variables. If a region variable in the return type of a function is quantified it means the region is ''fresh'', ie the data was allocated by the function itself. 

Notice that in the type of `succ`, both `%r1` and `%r2` are quantified, this means that `succ` accepts data from any region and returns a freshly allocated `Int`.

`sameInt` just passes its data though, so the same region is on both argument and return types.

`pi` is just static `Float` and not a function that does allocation, so it doesn't have a `forall`.

== Region classes ==
In Haskell we use type classes on type variables to restrict how these variables can be instantiated. For example, we can write:
{{{
(==) :: forall a. Eq a => a -> a -> Bool
}}}

Here, the `Eq a` context restricts `forall a` to just the types that support equality.

In Disciple, we can do a similar thing with regions:

{{{
csucc :: forall %r1 %r2
      .  Int %r1 -> Int %r2
      :- Const %r1
}}}

The ''region class'' constraint `Const %r1` restricts `csucc` so that it only accepts arguments that are constant. Data in `Const` regions is guaranteed by the type system never to be destructively updated. In Disciple we write the class constraints at the end of the type for clarity, though there is a plan to allow the standard Haskell syntax as well.

The opposite of `Const` is `Mutable` and we can explicitly define data values to have this property.

{{{
counter :: Int %r1 :- Mutable %r1
counter = 0
}}}

Any `Int` that is passed to `csucc` is required to be `Const`. If you try and pass a `Mutable` `Int` instead it will be caught by the type system.

{{{
main () = putStr $ show $ succ counter
}}}

{{{
   ./Main.ds:...
       Conflicting region constraints.
                 constraint: Base.Mutable %1
            from the use of: counter
                         at: ./Main.ds:...

        conflicts with,
                 constraint: Base.Const %2
            from the use of: succ
                         at: ./Main.ds:...
}}}

== Effect purification ==
Besides manually added annotations, the main source of `Const` constraints in a Disciple program is the use of laziness. Remember from [wiki:Language/Overview/EvaluationOrder EvaluationOrder] that the suspension operator `(@)` maps onto a set of primitive `suspend` functions.

If we wanted a lazy version of `succ` that only incremented its argument when the result was demanded, then we could write it like this:

{{{
lazySucc x = (+) @ x 1
}}}

this is desugared to:

{{{
lazySucc x = suspend2 (+) x 1
}}}

where `suspend2` has the following extended type:

{{{
suspend2
	:: forall a b c !e1 !e2
	.  (a -(!e1)> b -(!e2)> c) -> a -> b -> c
	,  Pure  !e1
	,  Pure  !e2
}}}

Now the addition function `(+)` for `Int` has this extended type:
{{{
(+)  :: forall %r1 %r2 %r3 !e1
     .  Int %r1 -> Int %r2 -(!e1)> Int %r3
     :- !e1 = !{ !Read %r1; !Read %r2 }
}}}

Which says it reads the two arguments and returns a freshly allocated `Int`

When we pass `(+)` as the first argument of `suspend2` the type system encounters the ''effect class'' constraint `Pure !{!Read %r1; !Read %r2;}`. This is then satisfied by constraining `%r1` and `%r2` to be `Const`. If a value is in a `Const` region then it is guaranteed never to be destructively updated. This means that it doesn't matter when we read it, so the operation is pure.

To say this another way, when a function application is suspended the type system ''purifies'' its visible `Read` effects by requiring the data being read to be `Const`.