Linear & Dependent types of ATS applied to the Cairo graphics library

I'm on the ATS mailing list, as I suspect other LtUers are, and saw this:

I find that cairo is a package for which it is fairly easy to put an
API in ATS. So if you have in mind a package for which you would like
to add an API in ATS, it may help if you take a look to see how cairo
is handled
. The rule of thumb here is to use linear types as much as
possible to track resource usage statically; dependent types can always
take the back seat :)

It seems like ATS is a pretty pragmatic / practical implementation of advanced type systems, from what little I've heard about systems which support such things. There's a paper about using ATS to implement Linux device drivers, for example.

(If only ATS could talk to C++, or if only Felix was done, or if only C++ cough cough was different. :-)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

RAII

While I'm sure there are plenty of valid uses for linear types, I kind of get the feeling that in this particular case, RAII like in C++, or even a function "with_cairo_surface :: (cairo_surface -> a) -> a" would be a lot simpler.

I guess it's when the value has a longer life than its function that this really 'shines'?

Not safe

Neither of your suggestions works properly. RAII only works in C++ because most programs are predominently first-order (and it still isn't safe) - it is not an option in a high-level language where closures are omnipresent and life time is not bounded by lexical scope. A with_* style function may help to prevent simple accidents, but also isn't safe, since nothing prevents a client from returning the surface from the argument function. That is, in both cases the resource could be accessed after it has been released.

For concreteness...

...here's a simple example illustrating Andreas's point:

  val with_surface : (surface → 'a) → 'a 

  let bogus : surface = with_surface (fun x → x)

So by instantiating the polymorphic type at type surface, you can pass it the identity function to get ahold of a deallocated surface.

We're talking about an

We're talking about an IO-oriented library here... You could always make sure the function returns (), if side effects are typed. In the general case, that doesn't work, of course.

Too constrained

Returning () would be quite constrained, even for I/O — it may work for the O side, but certainly not for the I side, where you usually want to get back some useful information.

Thanks

Thanks for the explanation - I appreciate it

This is still unsafe

References are very powerful!

  val with_surface : (surface → unit) → unit

  let stash = ref None  

  let evil(surface) = (stash := Some surface)

  let bogus : surface = begin
     with_surface evil;
     let Some(s) = !stash in
     s
   end

True, but

True, but pkhuong was careful to say "if side-effects are typed". In that case, I assume, your `evil' would not return type () as such. Although in that case, you probably cannot use the approach for I/O either.

It's the indefinite lifetime...

...of references that's the problem. Even if we give this API a monadic type, a monadic program can still get ahold of a stale reference:

   val with_surface : (surface → IO unit) → IO unit

   let bogus : IO(surface) = 
     do stash ← ref None;
        let evil(s) = stash := Some None;
        () ← with_surface(evil);
        Some(s) ← !stash;
        return s

Something like Haskell's runST would probably work, in which you add an extra index to the monad to tag the region of the heap the program should act on, and require the argument to be polymorphic in the region. But this isn't that simple; we're really nearing the point where linear types are just as easy to implement, and likely more flexible in practice.

Yes to all that

Yes to all that, but I was interpreting the parent post as suggesting that the user function has to return pure type unit, and not IO unit or anything similar, which would rule out any such examples (while also making the idea useless for I/O).

PS: hey, why unicodify your left arrows, but not the right ones? :-)

I figured he couldn't mean

I figured he couldn't mean that, since it would be useless for IO. :)

Anyway, I unicoded the left arrows since leading left-angle brackets trigger HTML parsing nonsense. But there's no reason not to unicode both arrows, so I changed them all. :)

OT

What's weird is that, on my Mac at least, the larr's appear to be twice as long as the rarr's. 8-} Does the Courier font include right arrows, but not left arrows?

Re: OT

the reason is that computers suck, i think. on this mac + ff, they look to be the same size to me.

Safe resource handling is already possible in Haskell

Something like Haskell's runST would probably work, in which you add
an extra index to the monad to tag the region of the heap the program
should act on, and require the argument to be polymorphic in the
region. But this isn't that simple; we're really nearing the point
where linear types are just as easy to implement, and likely more
flexible in practice.

Something like Haskell's ST does indeed work, and it is that simple --
provided our regions are isolated. However, often we would like to
access reference cells/file descriptors of parent regions in child
regions. Also, we would like to avoid imposing the total order on
parent regions. Even that is not enough for practical programs -- for
example, a child region may want to allocate a file descriptor in a
parent region, so that it can return it or put in a reference
cell. All these points have been described in the Lightweight Monadic
Regions paper (Haskell Symposium, 2008). The implementation --
surprisingly quite simple -- is available on Hackage and has been used
in a Safe USB library by Bas van Dijk:

http://hackage.haskell.org/package/usb-safe-0.4

Haskell already has all the required machinery for the discussed
facility (safe IO), and it seems quite easy to implement and use.