Importing instantiation of the parameterized module doesn't make those values available

[ajayeeralla]

//parameterized module
module M where
parameter
  x : [10]
type y = 10

//instantiated module
module N=M where
x = 20

// importing instantiated module
module O where
import N
// but I'm not able to access x value here for some reason

[weaversa]

Parameters are kept private. If you want to expose them, you can do something like this:

//parameterized module
module M where
parameter
  _x : [10]
type y = 10
x = _x

//instantiated module
module N=M where
_x = 20

// importing instantiated module
module O where
import N
// Now you can access x

[ajayeeralla]

Ah, I didn't know that parameters are private and the above example works. Thanks @weaversa.

I have another question:

module M where
type x = 10

module N where
import M 
type y = 20

module O where
import N
// but I'm not able to access x here but y only
// to access both x and y, I had import both M and N in this module

it seems to me that module importation isn't transitive?

[weaversa]

Yes, this helps keep the namespace under control.

[ajayeeralla]

I see. Thanks

[Frank-Zeyda]

Hi @weaversa, I stumbled across the above problem of module import not being transitive, and spent an afternoon until I stumbled across this issue that mentions the non-transitivity. I really feel module (and functor) import ought be transitive—that's what users I presume expect if nothing else said. Otherwise, the manual ought mention that in capital letters, i.e., in https://galoisinc.github.io/cryptol/master/Modules.html.

It is, of course, possible to work around the lack-of-transitivity issue but this gets very messy if one tries to build deeper hierarchies of (patametrized) modules, i.e., to capture product lines of cryptographic algorithms build on top of a hierarchy of algebraic structures to instantiate those algorithms. (Finding a solution for #1699 would also be excellent and useful in that context.)

My question: Would it make sense to reopen this issue?
Cheers—Frank (Galois IC)

[sauclovian-g]

Mostly you don't want imports to be transitive, but sometimes you do; this is why ML has both open (which is like import) and include. As far as I know Cryptol doesn't have any equivalent of include, but maybe it should.

Meanwhile, can you file a new issue about the docs?

[Frank-Zeyda]

Thanks David, having an include in addition to import would be fantastic. Yes, I can see that the need for transitivity wrt import depends on the use case, i.e., it is surely easier to keep the namespace clean if a priori imports are non-transitive. But having the option to decide would be an ideal solution.

PS: I will file an issue about the docs later on today! Cheers—Frank

[weaversa]

Cryptol absolutely already has include. After 20 years of programming Cryptol, I don't think it has a use. A robust module system should make include unnecessary. After 8 years and two (maybe three) module system iterations it is personally frustrating to see folks advocating for include.

IMHO (soapbox!) -- parameters should be public. It is idiomatic is Cryptol (and many other languages) to import modules as qualified, pulling in only what you need -- namespace pollution is not a strong argument here (above, I was parroting guidance I was given, that doesn't mean I agree with it). I believe #1699 is the current attempt to fix this wart -- a recent example: https://github.com/GaloisInc/cryptol-specs/blob/0278cf946f1f419c42533bac7980e04465899389/Primitive/Keyless/Hash/SHA2Imperative/SHA.cry#L61)

[yav]

The include in Cryptol is like #include in C. The one @sauclovian-g is talking about is in the ML module system, and it works differently---it is more like "import and re-export a bunch of stuff".

The current plan is to do #1699 indeed, we just need to find the resources to fix it. I don't believe it should be complicated to implement, as nothing major should change.