Back to Questions
1.2k
views3
comments
Purity. Liveness?
f#

Hello,

Is there a way in F# to require that a callee function be pure?

I'm exploring the possibility of a host that can require purity of its guest functions. Then, any IO or other side-effecting functionality must be requested to the caller through monads.

Bonus would be a way to test for liveness properties of the callee to guarantee termination. I'd be ok with certain restrictions as a compromise for this guarantee.

The goal here is a runtime or static verifiably (through the type system?) executionally safe but flexible way of transforming a state. This transforming function 1) must be pure and 2) must terminate.

Thanks,

Noob

.

In vanilla F# coding this is not possible.

There are various approaches to restricting what can be done with code. First you can use and interpret F# quotations (e.g. see [link:tomasp.net]). Second, you can simply define a resitricted datatype (DSL) that lists a compositional collection of operations for use with your host. That is, you'd represent your code as a data structure, and require that any code coming into your system simply creates an instance of this data structure, and then interpret that data structure.

However, these require a bit of engineering. So, in practice you might consider running the code in a .NET application domain with restricted security priveleges, or even in a separate process with different user-level permissions. These are the normal approach to achieving isolation on .NET

Kind regards

don

By on 6/8/2008 12:05 AM ()

Hi Don,

Thanks for the reply! Great work you're doing. And I really appreciate the time you take with the Channel 9 folks - really helps the learning process.

I'm down with your quotations approach (similar to your async workflow, except I want to be able to persist the state to disk and revive later). As I understand it, the quotation gets converted to a computational expression similar to .Net 3.0's ExpressionTrees, only more powerful. But once the F# compiler converts the code to data, I could hand it off to C# where I'm more comfortable, evaluate the computational expression, and either execute it directly from C# if the libraries offer that, or send it back to an F# module for execution. (Or maybe I just stay in F# the whole time. Whatever).

But here's my remaining forseen hang-up: What is it checking for? How would a computational expression tree crawler go about verifying purity? Is it as simple as disallowing assignments and requiring that called functions are marked with a PureAttribute as trusted by the host?

If this is a very complicated answer, do you at least have a book recommendation for me?

Thanks,

JDK

By on 6/17/2008 11:45 AM ()

FEI - I found some details at:

[link:en.wikipedia.org]

under "referential transarency" rather than purity.

By on 6/19/2008 10:33 PM ()

    Topic tags

    IntelliFactory Offices Copyright (c) 2011-2012 IntelliFactory. All rights reserved.
    Home | Products | Consulting | Trainings | Blogs | Jobs | Contact Us | Terms of Use | Privacy Policy | Cookie Policy     		Built with WebSharper