[IFC] support labels with parametrically polymorphic parameters

[tiziano88]

At high level, the proposal is to allow for "generics" as part of IFC principals (and therefore labels).

The definition of a principal would be extended to allow for "free" named parameters to appear in label definition and use.

Currently a principal may be of the shape A or A∨B or A∧B, where A and B are themselves principals (also recursively).

With this proposal, a principal may have zero or more "generic" placeholders that refer to other principals, e.g. A[X,Y] is a principal "template" A that has two parameters X and Y.

A template needs to be instantiated in order to be used, i.e. its parameters fully specified. So for instance, A[X=B,Y=C] (exact syntax TBD), where B and C are principals (recursively), is a "concrete" principal (this is similar to monomorphization / reification in type systems).

It is still unclear to me whether this can be implemented elegantly in the current IFC model in Oak, or whether we would need to move to a "more static" model first.

This is just the beginning of a discussion, a more detailed plan will follow.

cc @aferr @anghelcovici @seefeldb @bgogul

[seefeldb]

If we can find a mapping between this and the syntax notation, that would show that we can implement it with IFC (or it would show what is necessary to build it).

…

On Tue, Aug 18, 2020, 16:55 Tiziano Santoro ***@***.***> wrote: At high level, the proposal is to allow for "generics" as part of IFC principals (and therefore labels). The definition of a principal would be extended to allow for "free" named parameters to appear in label definition and use. Currently a principal may be of the shape A or A∨B or A∧B, where A and B are themselves principals (also recursively). With this proposal, a principal may have zero or more "generic" placeholders that refer to other principals, e.g. A[X,Y] is a principal "template" A that has two parameters X and Y. A template needs to be instantiated in order to be used, i.e. its parameters fully specified. So for instance, A[X=B,Y=C] (exact syntax TBD), where B and C are principals (recursively), is a "concrete" principal (this is similar to monomorphization / reification in type systems). It is still unclear to me whether this can be implemented elegantly in the current IFC model in Oak, or whether we would need to move to a "more static" model first. This is just the beginning of a discussion, a more detailed plan will follow. cc @aferr <https://github.com/aferr> @anghelcovici <https://github.com/anghelcovici> @seefeldb <https://github.com/seefeldb> @bgogul <https://github.com/bgogul> — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1371>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACN27X2BEVNOIUIZBP2N2DDSBMIG7ANCNFSM4QEJSGQQ> .