Personal tools

DDC/ClassSystem

From HaskellWiki

< DDC
Jump to: navigation, search

1 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.

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
much 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
.

2 Region classes

In Haskell we use type classes on type variables to restrict how these variables can be instantiated.

    (==) :: forall a. Eq a => a -> a -> Bool
The
Eq a
here restricts 'forall a' to just the types that support equality.

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

    succ :: forall %r1 %r2
         .  Int %r1 -> Int %r2
         :- Const %r1
The region class constraint
Const %r1
restricts
succ
so that it only accepts arguments which 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 (ticket) 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
succ
is required to be
Const
. If you try and pass a
Mutable
Int
instead it will be caught by the type system.
main ()
 = do   out $ 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:...

3 Effect purification

Besides manually added annotations, the main source of
Const
constraints in a Disciple program is the use of laziness. Remember from 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 type (ignoring closure information once again)
 suspend2
	:: forall a b c !e1 !e2
	.  (a -(!e1)> b -(!e2)> c) -> a -> b -> c
	,  Pure  !e1
	,  Pure  !e2
Now (+) for
Int
has this 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 ends up with an effect class constraint
 Pure !{!Read %r1; !Read %r2;}
which it satisfies by forcing
%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
.