User feedback suggests that it might be useful to allow interfaces that are parameterized by other interfaces. For example:
interface module I where
type n : #
type constraint (fin n)
interface module A where
import interface module I // This is the new feature
type x : #
type constraint (x <= n) // `n` is imported from `I`..
The idea is that an interface import would bring in some names in scope of the interface. Since interfaces do not contain values, we would only ever use the type parameters and constraints from the imported interface.
A parameterized interfaces is similar to a functor in that it cannot be used directly, instead we would have to first instantiate
it, for example:
interface module B = A{M}
The more common case, however, would be to instantiate interfaces with other interfaces, for example:
module A where
import interface I
import interface J { interface I } // interface `J` was parameterized,
// and we are passing in the parameters from `I`
Implementing this is likely closely related to fixing #1581
User feedback suggests that it might be useful to allow interfaces that are parameterized by other interfaces. For example:
The idea is that an interface import would bring in some names in scope of the interface. Since interfaces do not contain values, we would only ever use the type parameters and constraints from the imported interface.
A parameterized interfaces is similar to a functor in that it cannot be used directly, instead we would have to first instantiate it, for example:
The more common case, however, would be to instantiate interfaces with other interfaces, for example:
Implementing this is likely closely related to fixing #1581