Design of identType

[anton-trunov]

So far we have an idea that identType is a type T with a function fresh : seq T -> T with the property (fresh xs) \notin xs.

This, however, presents an issue: the fresh function needs to traverse its input list to generate a fresh value but if we need to call it repeatedly to generate a sequence of fresh identifiers, this resulting algorithm is going to be quadratic.

Instead, we could change the type of fresh to T -> T, i.e. we can generate a new fresh ident given the previous one. (So, for example, an instance of identType for nat would have succn as its fresh function.)

Let me outline several property statements that seem to be useful.

1. One of the most general ones (it only requires T to be eqType) could look like this (traject lives in Mathcomp's path module):

   forall (n : nat) (x : T), unique (traject fresh x n)

Basically, this says that all powers of fresh function produce distinct elements.
2. Another option (this would require T to be ordType) is to say

forall x : T, x < fresh x

3. And yet another option would be to make fresh of type nat -> seq T generating an n-tuple of unique identifiers:
   • forall n, size (fresh n) = n;
   • forall n, unique (fresh n).

[anton-trunov]

I had forgotten to mention this design makes it necessary to have an identifier to start from. This can be seen as an inhabited type but I'm not sure if identType should inherit from ihnType because

• extending the depth of a hierarchy involves some typechecking performance penalty;
• an inhabited type might have a default element which is not necessarily a good starting identifier.
  But I'm open to suggestions here :)

Btw, the previous version with fresh : seq T -> T kind of had this default element: fresh [::].

[volodeyka]

When we need to use the fresh element? --- at the moment when we try to add a new element in our exec_event_structure, when we want to expand it's domain. Since we don't want to use tuples for modelling finite functions, the domain of exec_event_structure won't be a tuple of sequence, but finSet. That's why if what to have a function that take not one element it must have type {fset K} -> K.
Also, If we have function of type fresh_motone : {fset K} -> K with property forall s (x : s), x < fresh_motone s we can easily obtain from it function of type K -> K with property formal x, x < f x, and vice versa for total orders (but not so easily).
Moreover if we have well-founded order we can obtain form fresh : {fset K} -> K with property forall s (x : s), f x \notin fresh s, fresh_motone : {fset K} -> K with property forall s (x : s), x < fresh_motone s .
So I think we need to ask for fresh_motone : {fset K} -> K because in concrete instances we often have total or even well-founded order

[anton-trunov]

We should be able to recover a function of type {fset K} -> K from the design I outlined (modulo some tweaks with regard to hierarchy). Looks like it's going to be quadratic, unless we ask identType to also be a join-semilattice, for instance in which case can fold the input container (a set, a list, ...) with join-operator and then get fresh on the accumulated result.

[eupp]

The whole point was to get rid of quadratic complexity. I think even the linear complexity is bad if we really care about the computational behavior :)
Thus, fresh needs to be constant time, and has to have type T -> T (i.e. it cannot consult the whole trajectory list, as it would imply the linear time or even worse).

[anton-trunov]

Right, but linear complexity is not enforced in the signature, that would be very cumbersome to do. The implementation proposed in PR #22 allows one to instantiate fresh with succn, for example.

[anton-trunov]

Btw, after sleeping on it, I propose to rename identType to freshType. For instance, this would be more in line with the corresponding Fresh Monad in Haskell: https://hackage.haskell.org/package/tamarin-prover-utils-0.8.5.1/docs/Control-Monad-Fresh.html.

[eupp]

Btw, after sleeping on it, I propose to rename identType to freshType. For instance, this would be more in line with the corresponding Fresh Monad in Haskell: https://hackage.haskell.org/package/tamarin-prover-utils-0.8.5.1/docs/Control-Monad-Fresh.html.

I kinda like identType more than freshType. But I agree we might need freshMonad in the future.
I'll try to explain my preferences for naming here.

identType is short for identifier type. It denotes that the type T : identType represents type that can be seen as a type of identifiers, i.e. collection of entities with certain properties.

freshMonad is the name of the monad. Generally, monads are used to model effectfull computation, and thus the name of the monad reflects the type of effects it can produce. freshMonad can produce fresh effect, i.e. it can allocate fresh identifier.

In short, the name identType better describes the entities (i.e. identifiers) that inhabit the type, while freshMonad denotes the type of the effect that monad produces.

[eupp]

I had forgotten to mention this design makes it necessary to have an identifier to start from. This can be seen as an inhabited type but I'm not sure if identType should inherit from ihnType because

* extending the depth of a hierarchy involves some typechecking performance penalty;

* an inhabited type might have a default element which is not necessarily a good starting identifier.
  But I'm open to suggestions here :)

Btw, the previous version with fresh : seq T -> T kind of had this default element: fresh [::].

BTW, I also was thinking about the possible instances of identType.
I can imagine two main instances.

• nat with fresh n := n.+1
• string with fresh producing some lexicographically larger string.

Now, for the second case, if we abstract string to just finite sequences of letters of some alphabet T, \i.e. the take the type seq T, we also have problems with seq T being an instance of inhType in the case when T is the empty alphabet.
The obvious solution is to consider empty string/sequence [ ] as a valid identifier, but I do not know would it be convinient for an end-user.

[anton-trunov]

In short, the name identType better describes the entities (i.e. identifiers) that inhabit the type, while freshMonad denotes the type of the effect that monad produces.

This makes sense, let's keep the name. Maybe just rename the file identtype.v to ident.v? (or identifier.v)

nat with fresh n := n.+1

Yep, this is the instance I provided in the PR.

we also have problems with seq T being an instance of inhType in the case when T is the empty alphabet.

I think this is fine, one wouldn't be able to introduce a proper fresh function for this singleton type.

[eupp]

ident.v is fine.

Looks like the only remaining problem is whether identType should inherit from inhType.
@anton-trunov how significant is the performance penalty. I thought that the packed classes idiom was invented specifically to fight this problem?

I agree that it might be too restrictive to assume that the default element from inhType is the starting identifier.
On the other hand, for two known insances, i.e. nat and seq T the 0 and [ ] are reasonable starting identifiers.
I think we need to think about other possible instances and use-cases before we made the final decision.

[anton-trunov]

I thought that the packed classes idiom was invented specifically to fight this problem?

Exactly. But it's no magic. The Mathcomp devs managed to curb the depth of their hierarchy at around 9. Proving usually requires deeper hierarchies compared to programming.

On the other hand, for two known insances, i.e. nat and seq T the 0 and [ ] are reasonable starting identifiers.

Indeed, sounds reasonable but if you aim at a reusable library I'm sure there will be a use case where is too restrictive for some one.

I think we need to think about other possible instances and use-cases before we made the final decision.

+1

[eupp]

A minor stylistic suggestion.
Can we agree to name the variables of type identType as id, id', id1, id2 etc, instead of ident and its variations?
The id is shorter and still has clear semantics.
If we will choose this convention, I would propose to rename ident0 into id0.

Other options for ident0 (if we don't want to have char 0 in the name) are first or start.

@anton-trunov @volodeyka @dmitromikh

[volodeyka]

A minor stylistic suggestion.
Can we agree to name the variables of type identType as id, id', id1, id2 etc, instead of ident and its variations?
The id is shorter and still has clear semantics.

id conflicts with identity function, unfortunately. And in most cases, we are looking at elements of identType as on events, and name them e, e1, e2... So maybe ident is better.
But if we want to somehow name a fresh identifier we can use something like fresh_id (in transitionsystem.v for example)