6
$\begingroup$

Consider this example on binary trees in some ML-like language:

type tree =
  | Null
  | Node of tree * tree

let rotate_left p =
  match p with
  | Null -> p
  | Node (a, q) ->
    match q with
    | Null -> p
    | Node (b, c) ->
      Node (Node (a, b), c)

In the definition of rotate_left above I only want to consider rotation on trees where the right subtree is also a node:

let rotate_left (Node (a, Node (b, c))) =
  Node (Node (a, b), c)

In relation to a ML-like type system, this second version of rotate_left is partial where as the first version is total.

Is there a type system expressive enough that such functions would be considered total?

Note; I use the term "subtyping" in the title of this question, since I think of the values of the type of the second version of rotate_left, to be a subset of the values of the type of the first version of rotate_left.

$\endgroup$
  • 1
    $\begingroup$ Welcome to CS.SE! Can you edit your post to clarify what your question is? I don't see a clear statement of the question. What precisely do you mean by "constrain a type by defining some context for it"? That could be easy or arbitrarily hard, depending on what kinds of constraints you want to encode. An example is not a substitute for a statement of what you are trying to achieve. What type systems have you already looked at? Have you looked at dependent types? Agda/Idris? Do you require a static type checker? Does it have to be decidable? $\endgroup$ – D.W. Feb 9 at 17:59
  • $\begingroup$ @D.W. thank you for the good points you made, I'll edit my question to try and address them $\endgroup$ – soren-n Feb 10 at 12:55
6
$\begingroup$

You want to write some executable code (is_left_restartable) and use it inside a type annotation. This is, by definition, a dependent type.

The problem when you have dependent types is that it's hard to keep type checking usable for a programming language. It's generally desirable to keep the type system decidable, because programmers tend to be annoyed when a programming error causes the compiler to loop forever. So at the very least the type constraints need to stick to a subset of the language that guarantees termination. And of course since type constraints are evaluated at compile time, they can't contain any side effects.

It isn't too difficult to define a subset of the language without arbitrary recursion. For example, just forbid recursive functions. And, to keep things simple, forbid the use of library functions or functions defined in a different module — if you don't do this then library functions need to be annotated, not only so that the type checker knows that they're allowed in types, but also so that the compiler knows what to make of them.

Even if type constraints are in a subset of the language that always terminates, that doesn't make them decidable. For example, if the type constraints can include enough arithmetic to encode addition and multiplication of variables — a context in which this comes up naturally is array lengths — then the type system encodes Diophantine equations and is therefore undecidable. It's possible to keep the system decidable if it only allows additions and not multiplications of variables, as in Dependent ML.

Even when type checking remains decidable, it's a lot harder to keep type inference decidable. That's not a big problem in itself, because programmers who want to benefit from the finer-grained types can just write type annotations. But it can be difficult to precisely define when type annotations are needed and when they aren't. It's still a difficult problem to find a good balance between requiring a lot of annotations, and making it easy for programmers to know when annotations are needed.

When the type constraints are purely defined in terms of pattern matching, as in your example, they can be expressed using generalized algebraic datatypes (GADT). GADT have matured enough to be supported in mainstream languages, notably OCaml. To avoid extensive analysis of which functions are allowed in types, most implementations of GADT including OCaml's use the type system to express constraints, not the term syntax. You would need to define is_left_rotatable as a type, and to write a transformation function from matching trees to is_left_rotatable.

$\endgroup$
  • $\begingroup$ thank you for the in-depth answer, I'll look into dependent types and GADT, they might very well cover my question, and if they do I'll be happy to accept this as the answer. If not then I'll have to refine my question to be more clear. $\endgroup$ – soren-n Feb 10 at 13:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.