Make all bindings opaque (formerly abstract) by default. In case of data declarations, restrict access to constructors to the module the type is defined in. In case of function declarations, make the binding irreducible/neutral for type-level evaluation/normalization/computation. Make bindings transparent (the opposite of opaque) with the attribute @transparent (alternative name floating around: @open (but what would its antonym and its hypernym be?)).
Nomenclature: Data type and function bindings are associated with a transparency: They are either opaque or transparent.
Intuitively, @public means making the type of a binding accessible to other modules and @public @transparent means making (the type and) the definition (constructors or expression) accessible to other modules.
Further, the type of @public bindings is not allowed to contain private bindings and the definition (the constructors or the expression) of @public @transparent bindings is not allowed to contain private or @public opaque bindings.
It should be an error to specify @transparent without @public (I think).
This is basically a copy of public in Idris (via):
Lushui: @public, Idris: export
Lushui: @public @transparent, Idris: public export
Implementation Steps
Remove @abstract
Add @transparent and implement constructor-hiding in the name resolver
Implement opaques-are-neutrals in the type checker
Open questions
Should @transparent be called @open?
Should we support restricted transparency e.g. @public @(transparent topmost)?
Make all bindings opaque (formerly abstract) by default. In case of data declarations, restrict access to constructors to the module the type is defined in. In case of function declarations, make the binding irreducible/neutral for type-level evaluation/normalization/computation. Make bindings transparent (the opposite of opaque) with the attribute
@transparent(alternative name floating around:@open(but what would its antonym and its hypernym be?)). Nomenclature: Data type and function bindings are associated with a transparency: They are eitheropaqueortransparent.Intuitively,
@publicmeans making the type of a binding accessible to other modules and@public @transparentmeans making (the type and) the definition (constructors or expression) accessible to other modules.Further, the type of
@publicbindings is not allowed to contain private bindings and the definition (the constructors or the expression) of@public @transparentbindings is not allowed to contain private or@publicopaque bindings.It should be an error to specify
@transparentwithout@public(I think).This is basically a copy of
publicin Idris (via):@public, Idris:export@public @transparent, Idris:public exportImplementation Steps
@abstract@transparentand implement constructor-hiding in the name resolverOpen questions
@transparentbe called@open?@public @(transparent topmost)?