# DDC/ClassSystem

### From HaskellWiki

< DDC

## 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

forall

*fresh*, ie the data was allocated by the function itself. Notice that in the type of

succ

%r1

%r2

succ

Int

sameInt

pi

Float

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

Eq a

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

succ :: forall %r1 %r2 . Int %r1 -> Int %r2 :- Const %r1

*region class*constraint

Const %r1

succ

Const

Const

Mutable

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

Int

succ

Const

Mutable

Int

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 ofConst

(@)

suspend

succ

lazySucc x = (+) @ x 1

this is desugared to:

lazySucc x = suspend2 (+) x 1

suspend2

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

Int

(+) :: forall %r1 %r2 %r3 !e1 . Int %r1 -> Int %r2 -(!e1)> Int %r3 :- !e1 = !{ !Read %r1; !Read %r2 }

Int

(+)

suspend2

*effect class*constraint

Pure !{!Read %r1; !Read %r2;}

%r1

%r2

Const

Const

*purifies*its visible

Read

Const