Home

Welcome to the session wiki!

Notes - 22 November 2015 - 9:33 PM

Looking through the first two attempts at defining session types:

• I don't understand the benefit of having every operation its own type with no constructors. The result is a collection of types with no witnesses. If you want every operation to be it's own type, use Inductive with a single constructor. Still, I don't get the benefit unless you're trying to create a fixed point of the various types together.

• Dual looks good and defines when two operation types correspond to each other. You can specify two protocol signatures and determine if each of their operations has corresponding dual in the other protocol.

• Is Dual checked by the type checker or by execution? I think the latter. Is this the way it should be?

• What does execution look like?

• Think about threading an evidence bundle through protocol execution. Specifically, you're sending and receiving things of some type. What is that type? How might we prove or disprove that a resulting value is of that type? How does the type change from one send/receive pair to the next? I want to know from the typechecker that a resulting bundle is or is not well-formed. Then I want to instantiate that bundle with specific values.

• The values created by the constructed types are not themselves types. Specifically, (A :!: R) is not a type, but a value of type ProtoA. Can we make it a type? Can I say that a particular protocol is of this type? Let's leave things as they are and let (a :!: r) be sending an a of some type A to a corresponding receiver and then engaging in r. This is of type ProtoA. I want it to be of some type A!R where ! is a type operation. Specifically:

    (a :!: r):A!R
  

  where A is the type of the message and R is the assembled type of the following message sequence. If we do this, the type checker can now help determine if a specific message sequence is of the right type.

Notes - 22 November 2015 - 10:55 PM

• Your last point above is what bothered me the most about my initial encoding. The operators :!: and :?: constructed values, not types. I think it may be worth trying an encoding similar to Chlipala's certified type checker (copied here for convenience) :

6.5 A Type-Checking Example We can apply these specification types to build a certified type checker for a simple expression language.

Inductive exp : Set := | Nat : nat → exp | Plus : exp → exp → exp | Bool : bool → exp | And : exp → exp → exp.

Inductive type : Set := TNat | TBool.

Inductive hasType : exp → type → Prop := | HtNat : ∀ n, hasType (Nat n) TNat | HtPlus : ∀ e1 e2, hasType e1 TNat → hasType e2 TNat → hasType (Plus e1 e2 ) TNat ...

This creates a "type-language" and "value language", then links them with a HasType relation. In my next attempt, I'll try to mimic this for protocols.

I think it's interesting that traditional values (Nat, Bool) are mixed with operations(Plus, And) in the expression language. I can imagine a similar implementation for protocols, with values like Nonces and Signatures mixed with operations like send, receive, bundle, etc.

Notes - 23 November 2015 - 9:11 AM

I wrote the following before I read the above. Need to pull before I write... Regardless, I think we are generally on the same page.

It just struck me what you're trying to do with making the individual session actions separate types. I think you're trying to do exactly what I thought you should do - make ProtoA capture more than it currently does. If that's the case, then in the type A!R the ! operator is a type operator. Something like this:

Notation "x!y" := (send A R)

where A and R are types instead of constructors for ProtoA. If that's the case, then something like:

nat ! Session

would be the type of

3 :!: Eps

where 3:nat and Eps:Session. (Ignore the specifics of naming - we can clean that up.)

If we can prove something like:

forall s: nat!Session, (p s)

then we know something about all protocols of type s and can instantiate s for a specific protocol. That should give us something close to what we did in class for {n=m}+{n<>m} and {1=1}+{1<>1}.

For once, the Haskell might be leading us astray...

=======

Notes - 28 November 2015 - 8:00 PM

After playing around with the Chlipala-inspired "HasType" model (See module "try3" in Session.v) that links protocols with their type by our own custom-defined typing relation, I found it to be a little bit clunky. It would still be nice to check session types in the Coq type system directly: (i.e. be able to say "Check (3 ! Eps)" and have Coq return "nat :!: EpsT". I think the only way to do this is to define distinct Inductive types for each session type.

I just pushed a new Session.v with new modules "try4" and "try5". try4 was a quick attempt to make each of the session types a distinct inductive data type. Basically, I tried to emulate the definitions in the Haskell implementation. For instance, the send session type is defined as follows in Haskell: "data (:!:) a r". The paper confirms that the session datatypes "require no constructors because they will have no runtime representation". This makes sense, since the computation will happen at the type level (the Monadic send/receive operations will thread the type). However, in Coq, it feels weird to use an inductive data type with no constructors(definitions require vacuous matches). I couldn't find a good way to "transform" the type upon each send operation.

Moving on to module "try5". Here, again, I gave each session type its own inductive type. But this time, I also gave each a single constructor. With this encoding, I could define a send operation with a reasonable type: "(A :!: R) -> R". Building values of these types is still a little bit clunky, however. One "gotcha" is that the constructors for the session types SendT and RecT (sendC and recC respectively) require the A and R type parameters, in addition to their concrete values. There may be a way to use type inference to clean this up. I also defined the Dual relation fairly easily: Although its surface type seems overly general (Type -> Type -> Prop) it only has evidence constructors for the session types.

I think module "try5" is closer to what we want. The main things that bother me are as follows:

1. It still feels clunky to build concrete protocols
2. Although the receive session type captures that the protocol should receive something of type A, this value seems to disappear in the implementation of the receive operation (See code comment above the receive operation)
3. How do we incorporate these types and operations in a Monadic framework?