The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

It is not enough. I want to use only the facts of finite maps to prove my 
properties and allow others to instantiate my proofs with their own (possibly 
better) implementations of finite maps. I can't even use the implementations 
present in the theories as they are since they are wrapped in modules and 
make their type constructor opaque.

Alists are an option, but aren't necessary. For example, Adam Chlipala used 
lists as the representation for his closures' environment component and 
indexed into it using the DeBruijn indicies of his identifiers. That's too 
much marriage to implementation details for me.

-Ian
----- Original Message -----
From: "Pierre Courtieu" 
<Pierre.Courtieu AT cnam.fr>
To: "J. Ian Johnson" 
<ianj AT ccs.neu.edu>
Cc: 
coq-club AT inria.fr
Sent: Monday, July 2, 2012 10:38:00 AM GMT -05:00 US/Canada Eastern
Subject: Re: [Coq-Club] Abstracted type constructors and positivity 
restrictions?

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