The Coq mailing list

["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.

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

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