Parameterized Modules and Type Exports

[WeeknightMVP]

Consider the following parameterized module and instance thereof:

module ParMod where
  parameter
    type p: #
  
  f : [p] -> [p]
  f x = x

module ParInst = ParMod where
  type p = 1

So far, so good. But suppose we want a module that reuses p...

module OtherMod where
  import ParInst
  
  g : [p] -> [p]
  g x = reverse x

cryptol> :l OtherMod.cry 
Loading module Cryptol
Loading module ParMod
Loading module ParInst
Loading module OtherMod

[error] at ./OtherMod.cry:4:8--4:9 Type not in scope: p
[error] at ./OtherMod.cry:4:15--4:16 Type not in scope: p
cryptol> 

Omitting g and then browsing (:b) reveals that f is in scope with type [ParInst::p] -> [ParInst::p], but p is not. I think p, being in the public scope of ParInst, should be in scope, as it would be for non-parameterized modules:

module NonParMod where 
  type p = 1
  
  f : [p] -> [p]
  f x = x

module NonParInst where
  import NonParMod
  
  g : [p] -> [p]
  g x = reverse x

Cryptol> :l NonParInst.cry
Loading module Cryptol
Loading module NonParMod
Loading module NonParInst
NonParInst> 

This example is based on an attempt to define a hierarchy of SHA-2 specs with a parameterized module SHA, instances SHA_256 and SHA_512 thereof, and truncated variants that import the instances, overriding digest size s but reusing initial hash H0, iteration constants K, etc.

[yav]

The current design is like this, as it wasn't clear that one would always want to export the parameters--- perhaps they are just an implementation detail? If you do want to export them, then you can do so via a type synonym. For example:

module A where
parameter type P : #
type N = P
f : [N] -> [N]

module B = A where
type P = 8

module C where
import B
g : [N] -> [N]
g = f

So basically, top level things fall into 3 categories:

1. public declarations,
2. private declarations, and
3. parameters.

Does that seem reasonable?

[WeeknightMVP]

Yes, this seems reasonable. Thank you for clarifying.