ta0kira / zeolite

Zeolite is a statically-typed, general-purpose programming language.
Apache License 2.0
18 stars 0 forks source link

Remove param-filter checks where type instances are used as value types. #157

Closed ta0kira closed 3 years ago

ta0kira commented 3 years ago

See #45 for original discussion. tl;dr: We might be able to skip instance validation except for:

  1. @type-function calls.
  2. Direct @value initialization, e.g., Type<#x>{ foo }.
  3. Passing types as function params.

The rationale is that param filters are irrelevant outside of procedures that rely on them to be able to call @value and @type functions.

If a value or instance is converted to something else, the procedures still use the "real" underlying type, which means that you should be able to safely use that object if its param variance allows converting it to something that violates those filters.

concrete Type<|#x> {
  #x requires Formatted

  @category create<#y>
    #y requires Formatted
  (#y) -> (Type<#y>)
}

The following should be allowed, since any will never make it into Type without being passed in one of the three situations mentioned at the top:

Type<any> value <- Type:create<Int>(10)

I think the main risk here is updating the type system to skip the checks in most cases without missing bad param names.


Also in need of resolution: Do we need to validate instances used in the type filters themselves?

@value interface Base<|#x> {
  #x requires Formatted
}

concrete Foo<#x> {
  // Should any be allowed here?
  #x requires Base<any>
}

concrete Bar {
  // Should any be allowed here? (If not, filters in interfaces are useless.)
  refines Base<any>
}

Overall, I think the solution is this:

  1. Remove instance validation for type-instances used in inheritance and on the right sides of all param filters.
  2. Remove instance validation for variable, argument, and return types.
  3. Replace all of those removed checks with a version that does everything except look at filters, e.g., check category names, param counts, param names.
  4. Disallow param filters in interfaces. (The original reason for allowing them was the possibility of needing them to validate type-instances used in argument and return types.)