Importing Types

[aijony]

[The datatype] Foo is not importable because it is not reified and therefore not a Scheme type.

Originally posted by @johnwcowan in https://github.com/pre-srfi/static-scheme/issues/13#issuecomment-724318430

• Can someone import a type from a library?

• Do types live in function/variable namespace?

• Would two imported types with the exact definitions and name type check?

[mnieper]

• As far as type (constructors) are explicitly needed, they should be importable and exportable. The standard library would, for example, export a list type constructor. Type constructors could be renamed on import.

• As macro keywords and variables live in the same namespace, it is logical that types live in the same namespace in particular as macro expansion comes before type inference.

• I would say two types defined at different places are not equivalent even if they are of exactly the same shape. Note that names are nothing but smoke and mirrors in Scheme as they can be renamed on import and export and by macro transformers. A type should therefore not be identified by its name. Such a view is consistent with Scheme record types.

[lassik]

• As far as type (constructors) are explicitly needed, they should be importable and exportable. The standard library would, for example, export a list type constructor. Type constructors could be renamed on import.
• As macro keywords and variables live in the same namespace, it is logical that types live in the same namespace in particular as macro expansion comes before type inference.

Agree with all of the above.

• I would say two types defined at different places are not equivalent even if they are of exactly the same shape. Note that names are nothing but smoke and mirrors in Scheme as they can be renamed on import and export and by macro transformers. A type should therefore not be identified by its name. Such a view is consistent with Scheme record types.

Haskell and MLs deliberately distinguish between type aliases and "new types".

• In Haskell and SML, type makes an alias.
• In Haskell newtype and data make a new type; in SML datatype does.

If there are value constructors (defined for a sum type by data/datatype), their names are significant. The names should probably follow Scheme's ordinary identifier rules: importing (possibly under a different name) etc.

Static Scheme should probably also distinguish between type aliases and "new types".

[lassik]

In some of the code sketches we've been making so far, define-type-alias defines an alias, and define-union-type defines a new type.

So two constructors would be equal if the Scheme identifier at the head of each constructor is the same one. Likewise, the union type itself is identified by the identity of its identifier :D

[mnieper]

Type aliases may not even be necessarily part of the type language. Maybe we can push them up to the macro expansion layer. But it's too early to say anything about this, I guess. In any case, they are irrelevant to the semantics (and just for convenience, but for that they may be important), much like C's #define. :smiley:

[lassik]

It's probably worth preserving the names type aliases for better error messages, but I agree that they shouldn't matter for semantics.

[johnwcowan]

To answer the second question first: types are bound to identifiers, just as in R5RS + SRFI 9 and R[67]RS. Unfortunately, none of these say what the record type identifier is bound to. In many R6RS systems, it is a syntax keyword: in other systems it is bound to an object: a record instance, something system-defined, or even a symbol. The only thing you can do with it is use it to create subtypes by specifying it in the parent clause. SRFI 9 and R7RS-small do not have subtypes, so it can't even do that. So the utility of exporting it is quite limited.

In Steme we would certainly want to be able export a whole datatype, including all constructors and accessors. In Scheme, record types are generative: if you declare them twice you get two different types, and this rule should apply to Steme as well. So if you want a Steme datatype to agree in two libraries A and B, then either A must import the type from B, or B must import the type from A, or both A and B must import it from some library C, as is already the case for Scheme.

[lassik]

In Steme we would certainly want to be able export a whole datatype, including all constructors and accessors.

+1, but I'd have the constructors exported separately from the type itself, which is simple and naturally matches Scheme semantics. This implies some constructors of a type can be "private" while others are "public", which is potentially neat. However, it's not clear how to print those "private" constructors from another library.

[mnieper]

To answer the second question first: types are bound to identifiers, just as in R5RS + SRFI 9 and R[67]RS. Unfortunately, none of these say what the record type identifier is bound to. In many R6RS systems, it is a syntax keyword: in other systems it is bound to an object: a record instance, something system-defined, or even a symbol. The only thing you can do with it is use it to create subtypes by specifying it in the parent clause. SRFI 9 and R7RS-small do not have subtypes, so it can't even do that. So the utility of exporting it is quite limited.

In R6RS, you can also extract a record-type descriptor and a constructor descriptor from the record name. Because all meaningful access to the binding of the record name is through the parent clause or special forms to retrieve the record-type descriptor and constructor descriptor, it actually doesn't matter to what kind of object the record name is bound to.

Unsyntax uses SRFI 213 properties to attach all the metadata to the record name, which is the clearest approach, I think.

In Steme we would certainly want to be able export a whole datatype, including all constructors and accessors. In Scheme, record types are generative: if you declare them twice you get two different types, and this rule should apply to Steme as well. So if you want a Steme datatype to agree in two libraries A and B, then either A must import the type from B, or B must import the type from A, or both A and B must import it from some library C, as is already the case for Scheme.

This use of the word "generative" is unfortunately not consistent with the use of the word in the R6RS. When people speak about generative Scheme record types, they usually mean that a new type is generated when the define-record-type definition is evaluated. This doesn't work well with a static type system, so what we want are nongenerative (in the sense of R6RS) record types.

These are generative in the sense @johnwcowan just used in that every lexical occurrence of a record-type definition stands for a new record type.

Apart from the wording, I totally agree. We just shouldn't it call "generative" to avoid confusion.

[mnieper]

+1, but I'd have the constructors exported separately from the type itself, which is simple and naturally matches Scheme semantics. This implies some constructors of a type can be "private" while others are "public", which is potentially neat. However, it's not clear how to print those "private" constructors from another library.

The printing problem has no good general solution and how to print types shouldn't be part of the final specification. The problem is that the (partially defined) map from identifiers to types is not injective.