Partial record type?

[weaversa]

Is it possible to specify a partial record type?

For example:

let f (x : {a : SetupValue, ...}) = ...

What if I just want to match on any record that includes a field named a of type SetupValue?

[weaversa]

Here's a more concrete example showing what I'd like to do. to_cryptol should take a list of values with t fields of type Term and return a list of the terms.

let pull_term (x : a) = do {
  return (x.t : Term);
};

let to_cryptol (x : [a]) = do {
  let ret = for x pull_term;
  return (ret : [Term]);
};

Here saw complains:

Record lookup on non-record argument.
Field name: t

[weaversa]

Maybe asking for 'shape' polymorphism on records is too much?

[atomb]

This sort of thing will become much easier using the Python interface. This would be a lot of effort to put into extending the language in ways we probably won't use in the long run.