Stream: Coq users

Topic: Shallow embedding of modules

Théo Winterhalter (Feb 03 2022 at 15:31):

Does anyone have references or tricks for doing some shallow embedding of module-like structures?
I mean structures that would define functions with potentially different signatures.

For now I use a map from names (nat) to ∑ A B, A → M B where M is a monad but when accessing a function in the module, you need to rewrite its type to use it.

Paolo Giarrusso (Feb 03 2022 at 18:31):

Wait, would you need to rewrite? Ensure the map is total and this should work fine.

Paolo Giarrusso (Feb 03 2022 at 18:33):

making the map total requires either replacing nat by fin.t size (likely a Sigma-based version), or making up fake entries. Either sounds preferable to a partial lookup.

Paolo Giarrusso (Feb 03 2022 at 18:36):

canonical structures are essentially records/sigmas + some inference for their use as modules, but it doesn’t sound like that’d help here…

Théo Winterhalter (Feb 03 2022 at 19:05):

No, the problem is that I pack the signature inside the value of the map, so when I do a lookup, I get a value of type ∑ A B, A → M B which I need to extract. Usually, I know the type I want to get from an interface, so I use this knowledge to extract the information and rewrite its type.

Paolo Giarrusso (Feb 04 2022 at 00:24):

Would something "hlisty" help? Take e.g. this (non-ideal) example:

Fixpoint hget (ls:list Set) (hls:hlist ls) (n:nat){struct n} : option (nth n ls Empty_set) :=  ...
(* from https://github.com/tidues/Heterogenous-List-in-Coq/blob/1609a7ff4db887ef27082953cd89120d66c69616/HList.v#L28 *)

Paolo Giarrusso (Feb 04 2022 at 00:24):

if you know the expected type, then ls is partially concrete so the return type would reduce.

Paolo Giarrusso (Feb 04 2022 at 00:25):

One can even use setups like with typed de Bruijn indexes — there, an environment is a heterogeneous list, and the position in the list is itself indexed by the type of the entry

Paolo Giarrusso (Feb 04 2022 at 00:26):

so you have things like lookup {gamma tau} : Env gamma -> Var gamma tau -> tau

Paolo Giarrusso (Feb 04 2022 at 00:27):

(and as you know you'd want Equations or Agda for most of this)

Théo Winterhalter (Feb 04 2022 at 06:30):

Right, that's an option indeed thanks.

The issue is that it's for exposing something to users so I was wondering if there was anything "transparent" where they wouldn't have to know about the encoding of variables. I guess not and I'll try out your suggestion. :)

Paolo Giarrusso (Feb 04 2022 at 11:13):

abstracting it into an hmap like HMap types -> Key types type -> type might at least hide de Bruijn from them... there might be a better kind of hmap but I'm not sure I'd know

Théo Winterhalter (Feb 04 2022 at 11:16):

Thanks a lot!

Last updated: Oct 04 2023 at 19:01 UTC