Go backward to Declaration Abstracts Go up to Top Go forward to Type Equivalence

Type Abstracts

D ::= ...| type I=T
T ::= nat | ...| I

D[[type I=T]] = lambda e. lambda s.
    ((updateenv [[I]] inType(T[[T]]e) e),
    (return s))

T: Type-structure -> Environment -> Store ->
    (Denotable-value × Poststore)
T[[I]] = lambda e. lambda s.
    cases (accessenv [[I]] e) of
        isNatlocn(l) -> (inErrvalue(),
            (signalerr s))
        ...
        [] isType(v) -> (v s)
    end

When are two variables equivalent in type?