The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

2012/7/2 J. Ian Johnson 
<ianj AT ccs.neu.edu>:
> Hello, I am trying to use the finite map theory (FMapInterface) in a theory 
> that reasons about explicit substitution semantics (e.g. the CEK machine of 
> Felleisen-Friedman). I am trying not to marry my reasoning to any one 
> implementation, for obvious reasons.
>
> There is a problem with this endeavor - the type of abstract maps on line 
> 62 of FMapInterface.v:
>
>   Parameter t : Type -> Type.
>   (** the abstract type of maps *)
>
> Has no definition-site positivity restrictions, so I cannot use t as a type 
> constructor in a mutually inductive way:
>
> Module CEK_fun (Names : DecidableType)
>                (Import fmap : FMapInterface.WS with Module E := Names).
>
> Inductive Value : Type :=
> | closure : lambda_expression -> Environment -> Value
> with Environment :=
> | mk_env : fmap.t Value -> Environment.
>

Hi,

> (* using list instead of fmap.t is completely fine - !! *)


Strictly speaking you won't use lists but *association lists* which
are implemented as an instance of FMapInterface in FMapWeakList.v and
FMapList.v.

This means that you can apply your functor (as it is) to obtain an
implementation using lists. Is that not enough for modularity? Maybe I
did not understand your question.

Hope this helps,
P.C.

> This completely defeats modularity, so that different theories of 
> collections cannot be effectively defined.
>
> What is the plan for supporting this kind of abstraction? In the meanwhile, 
> how can I effectively work around this without having to import a specific 
> implementation?
>
> I have tried allowing heterogeneous types for the fmap, but instantiating 
> at Value causes a universe circularity.
>
> Thanks,
> -J. Ian Johnson