## type-declaration-types.api
## (C) 2001 Lucent Technologies, Bell Labs
# Compiled by:
# src/lib/compiler/front/typer-stuff/typecheckdata.sublib# Datastructures describing type declarations.
#
# In particular, the sumtype
#
# Type
#
# provides the value type bound by the symbol table
# for that namespace -- see OVERVIEW section in
#
# compiler/typer-stuff/symbolmapstack/symbolmapstack.sml
stipulate
package ip = inverse_path; # inverse_path is from src/lib/compiler/front/typer-stuff/basics/symbol-path.pkg package mp = stamppath; # stamppath is from src/lib/compiler/front/typer-stuff/modules/stamppath.pkg package ph = picklehash; # picklehash is from src/lib/compiler/front/basics/map/picklehash.pkg package pl = property_list; # property_list is from src/lib/src/property-list.pkg package sta = stamp; # stamp is from src/lib/compiler/front/typer-stuff/basics/stamp.pkg package sy = symbol; # symbol is from src/lib/compiler/front/basics/map/symbol.pkg package vh = varhome; # varhome is from src/lib/compiler/front/typer-stuff/basics/varhome.pkg package lnd = line_number_db; # line_number_db is from src/lib/compiler/front/basics/source/line-number-db.pkgherein
api Type_Declaration_Types {
#
#
# Not quite abstract types...
#
Label; # = sy::Symbol
Typescheme_Eqflags; # = List( Bool )
# Mythryl semantics distinguish types whose values
# may be compared for equality (e.g., integers),
# which get declared 'eqtype', from those which may not.
#
# This distinction dates from the original Definition of
# Standard ML. Maintaining this distinction at the surface
# syntax level complicates the syntax significantly and
# may be regarded as a design flaw. Recent type-theoretical
# treatments of ML semantics (e.g. Harper-Stone semantics)
# infer equality test support for a type silently without
# explicit user declarations. For the moment at least,
# however, the Mythryl compiler still follows the old syntax.
#
# The following type lets us record what we know about the
# equality properties of a type during the type inference
# process. YES and NO represent definite knowledge and
# INDETERMINATE means we haven't yet learned anything
# one way or the other. The remainder cover various
# special cases.
#
package e: api { # Give YES/NO/... their own little namespace.
#
Is_Eqtype
= YES
| NO
| INDETERMINATE # This was "IND", which I'm guessing was a cryptonym for "INDETERMINATE" -- 2009-03-21 CrT
| CHUNK
| DATA
| UNDEF
;
};
Literal_Kind
=
INT | UNT | FLOAT | CHAR | STRING;
# The following variable types are core to the
# Mythryl Hindley-Milner type deduction logic
# implemented by code centered in the vicinity of
#
# src/lib/compiler/front/typer/main/type-package-language-g.pkg # src/lib/compiler/front/typer/types/type-core-language-declaration-g.pkg # src/lib/compiler/front/typer/types/unify-typoids.pkg # src/lib/compiler/front/typer-stuff/types/type-junk.pkg #
# The canonical type inference progression is
# USER_TYPEVAR -> META_TYPEVAR -> RESOLVED_TYPEVAR.
#
# Type variables supplied by the user like the X in
# my (foo: X) = ... ;
# start out represented as USER_TYPEVAR records.
#
# When permitted by the "value restriction" (see is_value in type-junk.pkg),
# they get generalized to typeagnostic ("polymorphic")
#
# META_TYPEVAR records, which in turn become
#
# RESOLVED_TYPEVAR records once we've inferred a complete type for them.
#
# INCOMPLETE_RECORD_TYPEVAR records are used to track incompletely specified
# records, canonically those declared using "..." ellipses.
#
# LITERAL_TYPEVAR records are used in inferring the types of literals like '0',
# which may resolve to any one of several different arithmetic types.
#
# OVERLOADED_TYPEVAR is used in resolving the types of + and other overloaded operators.
# The Bool value is TRUE iff it must resolve to an equality type.
#
Typevar # Used (only) in Typoid case TYPEVAR_REF to represent what we know so far about a type.
#
#
= USER_TYPEVAR {
name: sy::Symbol, # X or such. Construct via sy::make_typevar_symbol.
eq: Bool, # Must it resolve to an 'equality type'?
fn_nesting: Int # Outermost fun/fn lexical context mentioning/using us.
} # fn_nesting = infinity for type variables like X.
# # fn_nesting < infinity for fun/fn arguments.
# A user type variable like 'X' which
# has not been generalized into a
# META_TYPEVAR
# variable, either because generalization
# has not yet been done or because the
# type_junk::is_value() "value restruction"
# forbade doing so:
| META_TYPEVAR # A typeagnostic ("polymorphic") type variable. It expresses maximal ignorance: This is what we initialize a TYPEVAR_REF to before
{ # doing type inference on it -- see generalize_type' in src/lib/compiler/front/typer/types/type-core-language-declaration-g.pkg eq: Bool, # Must it resolve to an 'equality type'?
fn_nesting: Int # Outermost fun/fn lexical context mentioning/using us.
# fn_nesting = infinity for META-args
# fn_nesting < infinity for lambda bound
}
| INCOMPLETE_RECORD_TYPEVAR { # Used to represent a record type before we know all of its fields. For example if we see "foo.bar" we know 'foo' is a record, but the only field we know is 'bar'.
known_fields: List( (Label, Typoid) ),
eq: Bool, # Must it resolve to an 'equality type'?
fn_nesting: Int # Outermost fun/fn lexical context mentioning/using us.
}
| RESOLVED_TYPEVAR Typoid # When we resolve a META_TYPEVAR to a concrete type, we replace it by this.
| LITERAL_TYPEVAR { # Literals like '0' may be any of (Int, Unt, Integer, ...). We use this until the type resolves.
kind: Literal_Kind,
source_code_region: lnd::Source_Code_Region #
}
| OVERLOADED_TYPEVAR Bool # arg is TRUE iff it must resolve to an equality type.
# Represents overloaded operators like '+' which must be resolved at compiletime to concrete functions based on types of arguments.
# Overloaded ops are set up in src/lib/core/init/pervasive.pkg # and compiletime-resolved in src/lib/compiler/front/typer/types/resolve-overloaded-variables.pkg | TYPEVAR_MARK Int
#
# For marking a type variable so that it can be easily identified
#
# A type variable's REF cell provides an identity already, but
# since REF cells are unordered, this is not enough for efficient
# data package lookups (binary trees...).
#
# TYPEVAR_MARK is really a hack for the benefit of
# later translation phases, specifically:
# src/lib/compiler/back/top/translate/translate-deep-syntax-types-to-lambdacode.pkg # src/lib/compiler/back/top/translate/translate-deep-syntax-to-lambdacode.pkg #
# In any case, we should figure out how to get rid of it altogether. XXX BUGGO FIXME
also
Typepath
= TYPEPATH_VARIABLE Exception
| TYPEPATH_TYPE Type
| TYPEPATH_GENERIC (List( Typepath ), List( Typepath ))
| TYPEPATH_APPLY (Typepath, List( Typepath ))
| TYPEPATH_SELECT (Typepath, Int)
also
Typekind
= BASE Int # Used for builtin types like Char/String/Float/Exception -- see pt2tc in src/lib/compiler/front/typer-stuff/types/core-type-types.pkg | ABSTRACT Type
| SUMTYPE {
index: Int,
stamps: Vector( sta::Stamp ),
root: Null_Or( sta::Stamp ),
free_types: List( Type ),
family: Sumtype_Family
}
| FLEXIBLE_TYPE Typepath # "Definition of SML" calls typcons from apis "flexible" an all others "rigid".
| FORMAL
| TEMP
also
Type # Type is the referent for symbolmapstack_entry::Symbolmapstack_Entry.NAMED_TYPE
#
= SUM_TYPE # Used for raw::SUM_TYPE (==sumtypes) -- see type_sumtype_declaration in src/lib/compiler/front/typer/main/type-type.pkg Sumtype_Record #
| NAMED_TYPE { # Used for raw::NAMED_TYPE (not sumtypes) -- see typecheck_named_type() in src/lib/compiler/front/typer/main/type-type.pkg stamp: sta::Stamp, # stamp is from src/lib/compiler/front/typer-stuff/basics/stamp.pkg typescheme: Typescheme, # typescheme.arity gives the number of formals like 'X';
# # typescheme.body gives the 'THIS | THAT ...' info.
strict: List( Bool ),
namepath: ip::Inverse_Path # name is ip::last(path) -- the 'Foo' from Foo = ... or Foo(X) = ...
}
| TYPE_BY_STAMPPATH { # Used only inside apis
arity: Int,
stamppath: mp::Stamppath, # stamppath is from src/lib/compiler/front/typer-stuff/modules/stamppath.pkg namepath: ip::Inverse_Path # Name is ip::last(path) -- the 'Foo' from Foo = ...
}
| RECORD_TYPE List( Label )
| RECURSIVE_TYPE Int # Used only in domain type of Valcon_Info
| FREE_TYPE Int # Used only in domain type of Valcon_Info
| ERRONEOUS_TYPE
also
Typoid # Things which are type-like but not actually types, hence the name "typoid".
= TYPEVAR_REF Typevar_Ref
| TYPESCHEME_ARG Int # i-th argument to a Typescheme (qv)
| WILDCARD_TYPOID
| UNDEFINED_TYPOID
| TYPCON_TYPOID (Type, List( Typoid ))
| TYPESCHEME_TYPOID {
typescheme: Typescheme,
typescheme_eqflags: Typescheme_Eqflags # Records which Typescheme args need to resolve to equality types.
}
#
#
# Core types:
#
# o TYPEVAR_REF
# This marks the reference cells which get
# updated by the 'unify' operation during
# Hindley-Milner type inference. Once type
# inference is complete these are deadwood
# and we remove them at the first opportunity.
#
# o WILDCARD_TYPOID
# This matches anything during type inference.
#
# We use it, for example, for the return type
# of 'raise MY_EXCEPTION' statements: Since
# 'raise' in fact never returns it is ok to
# treat it as though it had whatever type the
# local context requires, possibly a different type
# each place it appears in the code.
#
# We also use it in error recovery. When a type
# has syntax errors we set it to WILDCARD_TYPE
# after issuing diagnostics, so that we can compile
# the rest of the file without generating spurious
# additional error messages.
#
# o TYPCON_TYPOID
# This represents a type constructor like List
# which takes one or more types as arguments
# and returns a new type: List(Int) and List(Float)
# are different types generated this way, for example.
#
# o TYPESCHEME_TYPOID
# See comments below at Typescheme.
#
# o TYPESCHEME_ARG
# This represents the i-th type argument to a typescheme.
# It will only appear within the body of a typescheme.
#
# o UNDEFINED_TYPOID
# This represents a type which we need to know but do not
# currently know. It is a compile error if we do not find
# a user definition of this type by the end of type inference:
# see for example make_record_pattern() and make_handle_expression()
# in src/lib/compiler/front/typer/main/typer-junk.pkg also
Typescheme
=
TYPESCHEME {
arity: Int, # Number of arguments
body: Typoid # Contains TYPESCHEME_ARG values marking where
} # fresh META typevars get inserted.
#
# Mythryl supports "don't-care" type polymorphism.
# "Polymorphic" literally means "many-shapes".
# A type-polymorphic function acts as though it
# has many types. (I prefer to call them "typeagnostic".)
#
# Type-agnosticism is what lets list::length()
# compute the length of a list of any type of value
# without triggering complaints from the typechecker.
# It is also called "parametric polymorphism" and
# "let-polymorphism".
#
# Type schemes implement typeagnostic types.
# The idea is that instead of assigning a typeagnostic
# function like list::length() a regular type,
# we assign it a "type scheme", which is essentially
# a type macro which we will expand into an actual
# type at each place in the code where the function
# is used. Since we can expand the "type scheme"
# macro with different type arguments each time,
# the function can behave as though it had a different
# type every time it is called.
#
# Our type schemes are essentially templates for producing
# regular types by plugging fresh META type variables into
# slots marked by TYPESCHEME_ARG values, a procedure
# implemented by
#
# instantiate_if_typescheme()
#
# from
#
# src/lib/compiler/front/typer-stuff/types/type-junk.pkg #
# For more background see the discussion near the top of
#
# src/lib/compiler/front/typer/types/type-core-language-declaration-g.pkg withtype
Valcon_Info # BAR in Foo = BAR This | ZOT That
= # Used in Sumtype_Member.
{ name: sy::Symbol,
form: vh::Valcon_Form, # Runtime form for valcon: tagged_int, exception , ...
domain: Null_Or( Typoid ) # 'This' in BAR This.
}
also
Sumtype_Member # Member of a family of (potentially) mutually recursive sumtypes.
=
{ name_symbol: sy::Symbol,
arity: Int,
is_eqtype: Ref( e::Is_Eqtype ),
#
is_lazy: Bool,
valcons: List( Valcon_Info ),
an_api: vh::Valcon_Signature
}
also
Sumtype_Family
=
{ mkey: sta::Stamp,
members: Vector( Sumtype_Member ),
property_list: pl::Property_List
}
also
Stub_Info
=
{ owner: ph::Picklehash,
is_lib: Bool
}
also
Sumtype_Record
=
{ stamp: sta::Stamp,
arity: Int,
is_eqtype: Ref( e::Is_Eqtype ),
#
kind: Typekind,
namepath: ip::Inverse_Path, # inverse_path is from src/lib/compiler/front/typer-stuff/basics/symbol-path.pkg stub: Null_Or( Stub_Info )
}
#
# The "stub" field will be set for any
# sumtype that comes out of the unpickler.
#
# The stub owner picklehash is the picklehash
# of the compilation unit on whose behalf this
# sumtype was pickled.
#
# Normally, this is expected to be the same as
# are the picklehash in the (global) "stamp", but
# there odd cases related to recursive types where
# this assumption breaks.
#
# (Is there a way of fixing this? -- David MacQueen.) XXX QUERO FIXME
also
Typevar_Ref # Used (only) in Typoid case TYPEVAR, to represent all we know so far about a type.
=
{ ref_typevar: Ref( Typevar ),
id: Int # Purely for debuggging printout purposes.
};
#
# The 'ref_typevar' above is the core hook for doing
# type inference via unification: Unification
# proceeds by re/setting these variables. The
# core unification code is in
#
# src/lib/compiler/front/typer/types/unify-typoids.pkg infinity: Int;
copy_typevar_ref: Typevar_Ref -> Typevar_Ref;
make_typevar_ref: ( Typevar , List(String)) -> Typevar_Ref;
make_typevar_ref': (Ref(Typevar), List(String)) -> Typevar_Ref;
# next_typevar_id: Void -> Int;
Valcon # Valcon" == "Value Constructor" -- "FOO' in "Foo = FOO".
=
VALCON { # The first three fields are the only ones that really matter:
name: sy::Symbol, # Name of valcon -- "FOO" value-symbol.
typoid: Typoid,
form: vh::Valcon_Form, # Runtime form for valcon: tagged_int, exception , ...
#
is_constant: Bool, # TRUE iff constructor takes no arguments -- e.g., TRUE, FALSE, NULL. (This field is redundant, could be determined from type.)
signature: vh::Valcon_Signature, # (Redundant, could be determined from type.)
#
is_lazy: Bool # Does valcon belong to a lazy sumtype? (Nonstandard undocumented extension.)
};
}; # api Types
end; # stipulate