Lambda the Ultimate

What would it mean to have 2 instances for the same type? I invoke function f on data d, which formula would be used to compute (f d)?

(Note after posting I saw the later comments below)

There would need to some way to pick. It could also be based on the context - if you're working in a context where some polymorphic type is only known to have a single instance, it makes sense to pick that one (even if the actual instantiated type has other instances).

Hi Tom,

Sorry for the delay in getting back to you. I was originally going to send you some Haskell code demonstrating my "Processes" and some text explaining their relation to monads & transformers and why I prefer them to that abstraction (and have some rough code if you'd like), but with my level of free time right now it might be a couple more weeks before I can do that. I think I can explain in a short description now, so here goes.

In section 6 of the "Datatypes a la carte" paper, the data type Term is essentially what I have in mind. As an aside and to shed light on my terminology, I prefer to work with Processes rather than Monads for reasons I'm working on expounding soon. Given a functor f, often built up through (:+:), I view (Fix f) as a non-terminating process that signals effects in f. Then, note that (Term f) is isomorphic to (Fix (Pure :+: f)), where Pure is a functor representing a simple effect that returns a result and aborts the current Process.

In your section 2.5, you note (in my words) the problem that all "state signals" go to the outermost state transformer. The most straightforward way to solve that problem would be to give it a type like (SMv Env m, SMm Reg m... => ...) that somehow instantiates the type class twice as SMv and SMm, and which lets instances of 'get' name which instance they intend to use. But Haskell doesn't let you do that.

So what I was proposing instead is to use a construction like Term from the a la carte paper, and have the State signal, which is reified to a functor under that approach, take another type parameter that names it.

So you end up with code like this (implementing only your Var expression - others similar):

data VarSt = VarSt -- This type serves as a name for a state signal
type instance StateType VarSt = [(String, Int)] -- Type functions used to encode the type of state this name uses

data VarEx = VarEx -- This type names the exception signal
type instance EndType VarEx = String -- This signal carries a String

evalVar :: (Signal ss, EndSignal VarEx :<: ss, StateSignal VarSt :<: ss) => Open e Var (ProcessK ss Int)

[Edit] Some details: You can take Process = Fix and Signal = Functor, data EndSignal n ss = Return n (EndType n) is a data type representing a signal of name n that ends the current process with a return code of type (EndType n), and data StateSignal n ss = ReadSt n ((StateType n) -> ss) | WriteSt n (StateType n) ss is a signal requesting either state read or write.

Here, ProcessK ss = Cont (Process ss) is simple type turning partial processes into a monad. Later on, when you want to interpret this ProcessK in a monad, you can peel off the translation to monad transformers with functions like this:

embedStateT :: Signal ss => n -> ProcessK (SignalState n :+: ss) -> StateT (StateType n) (ProcessK ss)

I haven't implemented that last one, but I think I got the signature right. Much of this other stuff I have implemented (though it's still possible that there are problems I haven't noticed).

Hopefully that's enough to clarify my cryptic earlier remarks to Philipa. Feel free to poke holes or ask questions. (I really did enjoy your paper, too!)

Best,
Matt

Hi Matt,

Thanks for your elaboration. If I understand your solution correctly, the essence of your approach is the use of global names (based on types) to tag each layer of your processes/monads. I believe this is essentially the same as Dan Piponi's tagged monad transformers layers which we mention briefly in our paper.

I think this solution provides less abstraction than the zipper because you resolve possible conflicts at the component level rather than the client level. Thus you may end up losing modularity. Also this approach is heavier than the zipper (at least for monad transformers), since we need more a bit more infrastructure in order to support the notion of tagged monad transformers.

Let me try to elaborate with respect to less abstraction:

Shall we use the same tag or a different one? - This is the design decision that we need to make when creating some more components using your approach. Let's for example add the "evalInc" component (see Section 5 of our paper). According to what you said "implementing only your Var expression - others similar", I'd say that you are suggesting that we have new tag's for for each of the layers. Something like this:

data IncSt = IncSt
type instance StateType IncSt = [(String, Int)]

data IncEx = IncEx
type instance EndType IncEx = String

evalInc :: (Signal ss, EndSignal IncEx :<: ss, StateSignal IncSt :<: ss) => Open e Inc (ProcessK ss Int)

But, if I understand your code correctly, this means that we will now have two environments and two exceptions: one environment and exception for the variable component; and one environment and exception for the increment component. If this is the case, that's probably not the behavior we want, at least for the environment, which is likely to be the same for both components (though this depends on the concrete application!).

One solution would be to use the same name in both components, which would solve the problem for applications which require the same environment for both components. However, this is making a strong commitment to using a particular layer. There are some situations in which you don't know which particular layer you'd like to use at the time of the definition of the component. For example, suppose that we wanted to have a simple tracing component, that would log every state change of a given variable. For this component your would use a Writer monad/process. However, we could have multiple different instances of the tracer component around, each tracing a particular variable. Now do you want to trace all the variables in the same Writer, or do you want to trace them on different writers? There's no good answer for what to do in this case, you may want to do it either way depending on the application/situation. Tagging your Writer monad for the tracing component with a fixed label, would force you to use the same Writer for all variables, which may be the wrong thing to do for a particular application.

I would say that the crucial point is that your approach tries to resolve conflicts early at the component level, whereas the zipper resolves conflicts later at the client level. If the goal is ultimate modularity then conflicts should be resolved as late as possible to allow for additional abstraction.

Hopefully I understood your solution correctly and my comments apply :). Otherwise, you can let me know what did I miss.

Bruno

Can we (probably using the zipper) 're-tag' transformers? It seems to me that tags are desirable either way.

Hi,

I agree that tagged transformers are a good idea and that they are nice to have. Note that in the previous text I was just emphasizing that, when ultimate modularity is the main goal, then the zipper seems to offer some additional flexibility/abstraction.

Views are closely related to tagged transformers, but they are more like local dynamic tags, rather than global static tags (see Section 5.2). Views are extremely flexible and allow for many interesting applications. Would they be helpful for the applications that you have in mind?

Bruno

I agree my approach is very similar to Dan Piponi's approach. I'm not sure, offhand, how to address your problem under his approach, whereas in my scheme it looks easy to address with a few methods like this:

combineEnds :: (Signal ss, EndSignal e0 :<: ss, EndType e0 ~ EndType e1) => ProcessK (EndSignal e1 :+: ss) a -> ProcessK ss a

Edit: Added missing type level variables 'a'

Does this not address your concerns? Or do you see some other problem with this approach?

First, I edited the signature above to use EndSignal rather than EndType on the RHS of =>. Hopefully my point came across.

Second, it seems to me that the approach I'm advancing here has an advantage over the zippers approach from a modularity point of view: it allows you specify that two signals be combined without implementing the environment for those signals. Of course, from a performance point of view it's just another layer of plumbing.

Hi Matt,

To tell you whether or not it works, I need to see the concrete implementation of the components and your combination function.

I have my doubts though, as it seems to me that with the type you have just written the only thing combineEnds can do is to drop the "EndSignal e1" part of the type-level list. If this is the case, and if I understand how the overall approach works, it seems like the wrong thing to do.

Maybe after you show us the details we can discuss it better.

Bruno

Hi Bruno,

First, imagine those were Processes, rather than ProcessKs. Then we just traverses the process, and for each signal matching (Inl (Return e1 v)) we construct (Return e0 v) and inject it into ss. Any signal matching (Inr ss) is kept as is. This defines the formula for an open function which we can fix.

To extend this construction to the ProcessK continuations, we take a tail (a -> Process ss), inject that tail to (a -> Process (End + ss)), use that tail to complete our original ProcessK and then apply the above construction on processes.

I think that'll work, but I'll send some code tomorrow and we can figure it out for sure one way or the other.

Matt