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.

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

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.

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

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.

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 *)
```

if you know the expected type, then `ls`

is partially concrete so the return type would reduce.

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

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

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

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. :)

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

Thanks a lot!

Last updated: Oct 04 2023 at 19:01 UTC