Plan for associated types (with @axch)

[dougalm]

co-written by @axch

Goal: Be able to define a type-class that models existence of a field-like thing in a record-like thing.

Non-goal: Fixing class methods referencing each other (this is orthogonal).

Non-goal: Good syntax for defining and using field accessors (this comes later, on top of the machinery below).

This touches Issue #710.

So, working around mutually-non-referencing methods, we would want to write something like this:

interface HasFieldType (a:Type) (l:Label)
  FieldType a l : Type

interface [HasFieldType a l] HasField (a:Type) (l:Label)
  getField l : a -> FieldType a l
  
instance HasFieldType (Point a b) 'x
  FieldType = a
  
instance HasField (Point a b) 'x
  getField = \(Point x y). x

Problem: Irreducible Types

When trying to do this, the first thing that goes wrong is type-checking getField: the type-level application FieldType a l cannot be reduced, because we don't know what a is.

Solution: Allow reduction of type applications to be deferred (operationally, this adds a TypeApp constructor to Atom). We can't quite maintain normalization during substitution, but we should be able to normalize "as soon as possible" enough for correct programs to type-check.

Specifically, these TypeApp constructors should only occur in the IR during type inference and simplification, because after simplification everything is monomorphic enough that they have all been normalized away (or an error has already been signaled).

N.B.: Syntactically equal type applications should type-check as equal; a normalized TypeApp should not type-check as equal to anything else.

Knock-on Problem: Useful error messages for irreducible types

We're only willing to do certain sorts of type reduction before runtime. If we have

def MyPairGood (a:Type) : Type = (a & a)
def MyPairEvil (a:Type) : Type = if expensive_computation () then a else Int

We're happy to reduce MyPairGood Int but not MyPairEvil Int. Currently, we attempt reduction during inference (when we see MyPairEvil Int) and report an error like "Can't reduce type expression: MyPairEvil Int".

But upon adding TypeApp, our type-producing functions can depend on dictionaries which remain unknown until the simplification pass. Consider a function like this:

def get_foo {a} [HasField a 'foo] (x:a) : FieldType a 'foo = getField 'foo x

Here, we can't reduce FieldType 'foo a until we have a concrete dictionary for HasFieldType a 'foo. We don't have that until we instantiate get_foo at a concrete type. That may occur at a call site for get_foo, or it may occur at a call site of a function that calls a function that calls get_foo. If that concrete type happened to define an evil FieldType method, the error will occur when it is finally reduced, and thus be much harder to trace than errors that can occur in the status quo.

Solution: Restrict Type-producing Functions

We'd prefer to have type-producing functions adhere to certain restrictions, such that reducing their application, once everything is concrete, always succeeds. Then we allow unreduced application of only such adherent functions, and our error messages will be local and good.

In particular, if MyPairEvil is tagged as a type-producing function, it will be flagged as error where it is defined; or if it is not so tagged, then any attempt to use it in a TypeApp will be flagged where it occurs.

Identifying Type-producing Functions

We can imagine a special sort of function syntax (like Haskell's type) to indicate that a function must be restricted in this way. But for now we're going to keep the current syntax, and identity type-producing functions as top-level functions with return type Type.

Validating Type-producing Functions

The test for validity-as-type-producing-function is
just that the body can be reduced as it stands (allowing for applciations of other type-producing functions to appear in the reduced type). This is quite restrictive, but it's already satisfied by every example in our corpus.

Note

This change is useful in its own right, because it will move the error about MyPairEvil to its definition even without any associated types.

Implementation Plan

1. Restrict type-producing functions as above, since that's useful in its own right.

2. Add TypeApp to Atom. The main sticky thing is normalization. Substitution can't maintain the normalization invariant because it can't pull dictionaries from the environment, so we have to normalize before pattern-matching on types. To make this not annoyingly expensive, we can either rely on Haskell laziness, or make an explicit normalizeShallow function that does what laziness does, namely normalizes until the top-level constructor is not TypeApp.

   We anticipate that we'll miss several places initially and there'll be bugs (of the "not implemented error" flavor) due to not normalizing where we need to. The good news is that only inference and simplification need to worry about normalization. After simplification, types are completely concrete (other than "data" parameters, like n in Fin n). And inference already has to reason about normalization today.

3. Make sure type-producing class methods are tagged and checked as type-producing functions (likely trivial).

4. Define HasFieldType as above and see whether it works on an example.

5. Think about surface syntax for making all this nice, syntehsizing instances, etc.

Knock-on Benefits

Maybe these valid-type-producing-functions can be re-used as user-defined patterns? They don't quite match the power of Haskell's pattern synonyms, but could be useful for something.

Restrictions remaining after this is implemented

Note that this won't give us associated types with the expressiveness that @tscholak was asking for in #710 and #709. It doesn't allow, for example, pattern-matching on types, or doing any nontrivial computation (like case analysis on an unknown constructor) to determine an associated type.