DDC/ClassSystem

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

Region classes

In Haskell we use type classes on type variables to restrict the types they can be instantiated by.

    (==) :: 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 function 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:...

Effect purification