Xen project Mailing List

On 20 November 2014 15:22, Anil Madhavapeddy <anil@xxxxxxxxxx> wrote:
>
> On 20 Nov 2014, at 14:47, Mark Florisson <mbf24@xxxxxxxxx> wrote:
>
>> This is very cool, so the idea is to have implementation
>> modules/packages declare that they implement a certain interface which
>> is provided as a separate package, and to have clients link to these
>> implementations either through functors or by explicitly resolving a
>> package ('cohttp<0.12')?
>>
>> The system you're proposing sounds like it is trying to provide
>> "strong modularity", where implementations depend only on interfaces,
>> and not on other implementations. There has been recent work on
>> Backpack in Haskell which is trying to provide this with the help of
>> basically a package DSL, where dependencies may remain 'abstract' to
>> be satisfied by some other package (in ML you'd use functors for
>> this).
>
> Right, except we're not proposing this system -- it's already how
> Mirage works.Â A unikernel is parameterised as a functor across Mirage
> module types (see the examples in https://github.com/mirage/mirage-skeleton).

Yeah, the system is very much inspired by mirage :)

> The question is how to break up the module types such that we can
> assemble them independently of each other as we upgrade the system.

Right, and I think there's two problems you're running in to, both with the structural subtyping that ocaml gives you, and the more nominal system that is being proposed (signatures in separate packages). To try and illustrate the point better, I've attached a crappy photograph :)

The thick edges represent a typecheck by the compiler at the definition site, which is sealing for the "Package" nodes, and functors for the "Client" nodes. The dotted edges represent things that are checked at useÂsites, that is, whenever you try to apply a functor.

The first diagram represents how we use structural subtyping, whereas the second represents nominal subtyping with signature packages. In either case, the relationship between the signatures and their corresponding newer version is entirely implicit. With structural subtyping, even the relationship between the Package and the Client is implicit. Now consider that we want to link Client-v1 to Package-v2.

With structural subtyping, all we can do is tell opam we need package v2, and apply the functor (and do some additional praying). With (true) nominal subtyping we can't perform the linkage at all, unless we specify that Package-v2 is also compatible with Signature-v1. However, this breaks functorization, since now we can't write a functor that requires something that isÂcompatible with both Signature-v1 and Signature-v2.

So I think version ranges are not only ad-hoc, they also impose unnecessary restrictions on modularity. For instance, version ranges allow you to link Package-v2 with Client-v1 (by specifying that Package-v2 implements both signatures), but I think they fundamentally break type sharing, and hence functorization. You can fix this problem in three ways:Â

Â ÂÂ

Â Â 1)Âgo back to structural subtyping -- write a functor that requires Signature-v2, and coerce the structure somewhere to Signature-v1Â

Â Â 2) allow version ranges within functor argument types to allow more precise constraints

Â Â 3) make backwards compatibility explicit at the signature level

Does that make any sense? :)

>>
>> I'm currently working on a module system in the trend of ML, that is
>> attempting to provide strong modularity for both packages and modules.
>> The main idea is to regard an interface as a specification that is
>> independent of any implementation (that either requires or implements
>> the functionality). Evolution of these interfaces can then be
>> specified explicitly, through a nominal subtype relation between the
>> different versions of the interface. Essentially, you can explicitly
>> declare that a newer version of an interface is backwards compatible
>> with an older one.
>>
>> Dependency resolution now only looks at interfaces, leaving versioning
>> with the job of pinning specific implementations and excluding buggy
>> ones. The nominal relation allows you to distinguish between semantic
>> changes, as opposed to more superficial structures changes.
>>
>> Concretely, it uses separate signature packages as you mentioned, e.g.
>> cohttp-types. You then have two ways of linking stuff: functors and
>> imports. Functors work like
>>
>> Â Âfunctor MyFunctor (set : SetSig) ...
>>
>> where SetSig refers to a signature package (in your configuration, you
>> might say SetSig=0.1). To then resolve concrete dependencies you do
>>
>> Â Âimport HashSet as (set : SetSig, eq : Eq)
>>
>> grabbing some version of HashSet that is compatible with the
>> interfaces SetSig and Eq. Both these constructs are a form of dynamic
>> linking. The first allows any compatible version of any
>> implementation, the second allows any version of a specific
>> implementation. This can be further constrained with versions in
>> configuration.
>
> I was nodding along until I saw the "dynamic linking" :-) ÂThe import
> that you are proposing is a combination of functor application and some
> selection of the implementation (in OCaml, this could be done via
> OPAM for example).
>
> The mirage frontend tool currently generates a main.ml that does the
> functor application, so you could frame it as a program stage rather than
> dynamic linking...

> -anil
>

Re: [MirageOS-devel] [ANN] IPv6 on Mirage!