AshleyYakeley / Truth

Changes and Pinafore projects. Pull requests not accepted.
https://pinafore.info/
GNU General Public License v2.0
32 stars 0 forks source link

Type variable quantification for record functions (and record constructors?) #312

Open AshleyYakeley opened 1 month ago

AshleyYakeley commented 1 month ago

Record Functions

Should be able to identify certain type variables in record functions. For example:

# implicit type form (matching var from sig) (disallow?)
f1: Maybe t of
    m: a -> (a *: t);
    end = ...;

# explicit type form (quantified)
f1: Maybe t of
    type t;
    m: a -> (a *: t);
    end = ...;

# explicit type form
f2: Integer -> Text -> Text of
    type t;
    m: Text -> t -> (t *: Text);
    end = ...;

# no quantified type
f3: Integer -> Text -> Text of
    m: Text -> t -> (t *: Text);
    end = ...;

Equivalent types:

Record Constructors

# implicit type form (already, matching var from sig)
datatype R1 +t of
    Mk of
        m: a -> (a *: t);
    end;
end;

# explicit type form (disallow?)
datatype R1 +t of
    Mk of
        type t;
        m: a -> (a *: t);
    end;
end;

# explicit type form
datatype R2 of
    Mk of
        type t;
        m: Text -> t -> (t *: Text);
    end;
end;

# no quantified type
datatype R3 of
    Mk of
        m: Text -> t -> (t *: Text);
    end;
end;

Equivalent types:

Matching:

AshleyYakeley commented 1 month ago

To do: