Top-level constraints syntax

[maximemulder]

Allow writing subtyping constraints at the top level, which is not meant to appear in real programs but can be useful to write tests (I do that !).

Example:

Int <: [Bot <: Top] => Int
//│ OK

A & B <: A
//│ OK

:te
A <: A & B
//│ ═══[TYPE ERROR] Cannot solve judgment A ≤ A ∧ B.

[maximemulder]

Conceptually clean pattern but I must say the Scala syntax is so heavy here 😔

[LPTK]

How would you suggest to make it better?

[maximemulder]

I think it's mostly me being a x.type hater. I think values should be automatically lifted to singleton types when appearing in type positions. I also don´t like how Scala has both the bind @ pattern and bind : type syntaxes, the former should ideally subsume the later IMO. I also don't like how I had to use parentheses around the union.

[LPTK]

Yeah, all these things should be addressed in MLscript/Witt 😛

  InfixApp(lhs, Keywrd(Keyword.`<:` | Keyword.`:>` as op)), rhs) then
    Term.SubConstr of constraint(lhs, op, rhs)

(At least that's the syntax I envision.)

In Scala, x can't be used as a type due to the separate namespaces. When they introduced literal types, they briefly debated whether to make it 2.type (for consistency) or just 2, but they opted for the latter because it's just much nicer.

[LPTK]

Proposal: add to Predef

abstract class (<:<) Sub[A, B] with
  fun apply(x: A): B
abstract class (=:=) Eq[A, B] extends Sub[A, B] with
  fun apply(x: A): B
object Refl[A] extends Eq[A, A] with
  fun apply(x: A): A = x

[maximemulder]

@LPTK Should I also add a Sup[A, B] base class ? I kind of want two because I like having the two syntaxes (subtype / supertype), but not sure how to do it (the following example obviously fails) 🤔

abstract class (<:<) Sub[A, B] with
  fun apply(x: A): B
abstract class (>:>) Sup[A, B] with
  fun apply(x: A): B
abstract class (=:=) Eq[A, B] extends Sub[A, B], Sup[A, B] with
  fun apply(x: A): B
object Refl[A] extends Eq[A, A] with
  fun apply(x: A): A = x

[LPTK]

Should I also add a Sup[A, B] base class ?

Can you make it

type (>:>) Sup[A, B] = Sub[B, A]

?

IDK if this will work, but it should (if it doesn't, you could fix it).

[maximemulder]

@LPTK Using the following works but the precedence is higher than most other type constructs so I have to put parentheses around most types on each sides (unions, intersections, arrows...), do I just accept the drawback or do you have an idea to solve that?

abstract class (<:<) Sub[A, B] with
  fun apply(x: A): B
abstract class (=:=) Eq[A, B] extends Sub[A, B] with
  fun apply(x: A): B
object Refl[A] extends Eq[A, A] with
  fun apply(x: A): A = x

type (>:>) Sup[A, B] = Sub[B, A]

[LPTK]

Ah right, because the precedence is inferred from the first and last characters (< and >, here). I can see that it's not ideal, but maybe we can live with it for now?

[LPTK]

Otherwise LGTM.

[maximemulder]

Okay, I pushed a commit with the following changes:

• Add classes and type alias to model subtyping constraints in the prelude.
• Remove the <: and :> keywords in favor of the aforementioned types.
• Change the constraint syntax from <: / :> to <:< / >:>.
• Remove the Term.SubConstr term (constraints are now usual applications).

This simplifies the code at the cost of wrong/annoying precedence (requires parentheses for many composed types).

[LPTK]

Actually if precedence is that important, why don't you just use S extends T? It parses correctly.

[maximemulder]

@LPTK I think that would make the syntax of constrained and universal types ambiguous:

[A extends Int] => Int // Constrained or universal type (while the constraint is the same, should A be a new variable or not ?) ?

[LPTK]

Yes, but I was talking about your top-level constraint testing use cases.

The <:< class and its use in constrained types can remain the same.

[maximemulder]

Hhhhm, I just checked and actually it doesn't seem to work for the top-level case either:

(~Nat & Int) extends Int
//│ FAILURE: Unexpected compilation error
//│ FAILURE LOCATION: subterm (Elaborator.scala:581)
//│ ╔══[COMPILATION ERROR] Unexpected infix use of keyword 'extends' here
//│ ║  l.62: 	(~Nat & Int) extends Int
//│ ╙──      	^^^^^^^^^^^^^^^^^^^^^^^^
//│ FAILURE: Unexpected parse error

I can make it work but I think I will just accept to use parentheses IMO.

[LPTK]

Hhhhm, I just checked and actually it doesn't seem to work for the top-level case either

Well of course, since extends is a keyword, for that use case you'd need to adapt the Elaborator to handle it...

[maximemulder]

Edited my message at the same time as you sent yours 😅

Anyway, I kind of like having the same syntax for constraints in constrained types and at the top-level, parentheses are not that big of a deal IMO.