4
$\begingroup$

Pattern Types

I am coming from JS/Ruby-land, where in Rails you have things like validation that a string field on a data model matches the IP address regex, for example:

class UserData < ActiveRecord
  validates_format_of :ip, with: /^((25[0-5]|2[0-4][0-9]|[01]?[0-9][0-9]?)\.){3}(25[0-5]|2[0-4][0-9]|[01]?[0-9][0-9]?)$/
end

To me, you should be able to do this, and so there is no difference between a "validation" and a "type check":

if (isString(val)) {
  log('is string!')
}

if (isEmail(val)) {
  log('is email!')
}

The reason why isEmail isn't traditionally considered in the realm of typechecking seems to be because it's complicated (or impossible?) to check at compile time, no other reason. I feel like this could be addressed with dependent types, but (a) they are a little over my head, and (b) there isn't much in terms of knowledge out there on the web pn imperative (non-functional) programming and dependent types. But building off the example from here (I don't see how this could be done at compile time in any case, it seems like it should be done at runtime):

type BoundedInt(n) = {i:Int | i<=n}

# dependent type used
def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

You might have something like:

type Email(x) = {x:String and x.match(/regex/)}

def login(email: Email) =
  # do login

But then I imagine just reading a string from a file, which may or may not contain an email, and how would you know that other than at runtime.

let val = readFile('./foo.txt')
login(val) # what happens here?

So that is my part about pattern types (regexp being string patterns, but perhaps there are other patterns too).

Constraint Types

A "constraint type" then might be something where you have constraints on the values (maybe pattern types are one subclass of constraint type in this thinking, not sure).

type Color = {
  r: BoundedInt(256),
  g: BoundedInt(256),
  b: BoundedInt(256),
}

type LoginInfo = {
  pass: String
  passConfirm: String
    constraint: (self, val) => val === self.pass
}

type SomethingRandom = {
  a: Int
  b: Int
} where (self) {
  if (self.a > 100) {
    assert self.b === 12
  } else if (self.a > 10) {
    assert self.b === 32
  } else if (self.a === 4) {
    assert self.b === 42
  }
}

I can only imagine such things being done at runtime. Is it possible for these sorts of things to be done at compile time somehow?

Conclusion

Even if they can't be done at compile-time, and only can be done at runtime, couldn't we still call them "types"? Why do we consider String a type, but Email not a type? To me it seems because of convention or because it can't be done at compile time perhaps, but maybe there are other important less arbitrary reasons.

So the main question is, could a language have types such as these pattern/constraint ones like I've outlined? (Which only seem to be runtime-checkable)? Is it possible? If so, how and when would you do the typechecking, roughly speaking? If not, why not?

$\endgroup$
6
  • $\begingroup$ Yes. These are called refinement types. $\endgroup$
    – pxeger
    Jul 7, 2023 at 6:09
  • $\begingroup$ @pxeger can you go into more detail, and perhaps show an example or two, explaining how the compiler or runtime would handle them? Wikipedia offers no help here. I am particularly wondering for imperative programs (not functional ones). $\endgroup$
    – Lance
    Jul 7, 2023 at 6:10
  • $\begingroup$ I think it's called refinement type. Refinement type means that the type satisfies additional assertions, while dependent type means that the type depends on the value. Although the dependent type system can completely cover the refined type system in theory, it is not recommended to add additional complexity. $\endgroup$
    – Aster
    Jul 7, 2023 at 6:11
  • $\begingroup$ @Aster how is that possible with let email = readFile('./foo.txt'); login(email)? $\endgroup$
    – Lance
    Jul 7, 2023 at 6:43
  • $\begingroup$ ``` Email :: String<\x -> is_email x> Login :: String -> IO Email ``` $\endgroup$
    – Aster
    Jul 7, 2023 at 7:04

1 Answer 1

5
$\begingroup$

You can still call them types, and languages do. You've referred to dependent types already, but refinement types are the particular sort that are equipped with a predicate like a regular expression or a logical test. Constraint types is a fine description as well.

You can check more of these constraints statically than you might expect, though it generally requires use of theorem provers or such things as part of the typechecking, and often more annotation of the invariants you expect than just the types. Whiley is one language that does this while otherwise behaving like an ordinary programming language. It permits type definitions

type ArrayOfPositive is (int[] items) where all { i in 0..|items| | items[i] > 0 }
type pos is (int p) where p > 0

and it won't allow any non-positive value into an ArrayOfPositive, but will allow any value out of it to go into a pos-typed variable.

pos n = 3 will work, and pos n = -2 will not work, statically; a loop that counts down in a pos will be rejected if it doesn't provably stop in time, and the compiler will produce a counterexample. On the other hand, some properties can't be established so easily, and require run-time checks to establish that the type is met before a value is allowed to pass into it, either by the programmer or the system: if you test that i is positive, you're now allowed to put it into one of those arrays.

Building a theorem prover into your type checker is enough of a thing for that to be the thing that the language does. Verifying regular expressions is theoretically doable too, but probably a step too far for any nontrivial case, though precise flow-sensitive checks for an exact matching expression should be viable.


Other languages allow similar things with only run-time checking. Raku is one of these:

subset Positive of Int where * > 0;

defines a type Positive that only holds positive integers.

Raku permits some fairly extreme cases in the where clause, including something like subset F of Str where *.IO.f, which is the type of names of existing files, which can't possibly be validated at compile time. Given a declaration my F $x, assigning, say, an empty string is certainly an error, while any string that is a real file name works. This is checked every time dynamically, can be used in matching and overloading, and behaves exactly like a typical type in the system.

You can see where this could implement your email regex, too, but it goes beyond that — the type of a username that exists in the database is feasible, or even the type that is the password of that user. Any existing type can be restricted in this way. This leans fully into the dynamic testing path, beyond what even theorem provers are capable of showing statically.


It's also possible to allow arbitrary checker objects to be elevated to use as "types". This is the approach in First-Class Dynamic Types (my work and others'), which took a dynamic pattern-matching system and permitted those patterns to be used as types. They could enforce arbitrary constraints at run time, but without any innate static checking. Whenever a value passed through a type annotation, the pattern would be validated, and a dynamic type error raised if it didn't match. These are syntactically type annotations in the language, but the types are first-class values with arbitrary implementation code. There's a little more pushback on calling these "types", but it's essentially fair enough when they perform the same dynamic validation as any sound gradual type checker would.

If you want to allow any constraint at all to be representable as a named "type" value with run-time checking, this is a reasonable approach. Racket's dynamic contracts are another similar approach in a different style, and a number of multimethod languages like Thorn or Fortress permit overloading on dynamic constraints — not quite a "type", but directing the code into different implementations based on matching, or erroring out — so that you could have one "login" function for a valid address, and one for an invalid one, dispatched automatically. Simple integer range constraints with dynamic checking are quite common in Pascal derivatives as far back as Modula-3, and although not highly common you do see them in quite a few languages.

$\endgroup$
10
  • $\begingroup$ Excellent info, thank you! Clears a lot of stuff up for me. I guess Raku is more like what I was imagining, yeah proof checkers would be great except (a) it's way over my head and (b) it doesn't cover everything (like your where *.IO.f example). Is there a world where you could have as much of it possibly done statically, but the rest done at runtime? I guess that might be what Raku does. In that case, what is allowable statically, and what isn't is my related question (a big list). $\endgroup$
    – Lance
    Jul 7, 2023 at 7:10
  • 2
    $\begingroup$ Yes, you could, and some do - run the theorem prover statically, and any time you get a "maybe" (or things you can't possibly verify) you insert dynamic checks. One thing about the Raku system is e.g. if you delete the file after you put the value in, it won't notice — these are necessarily point-in-time checks, while sound static verification is a permanent guarantee. $\endgroup$
    – Michael Homer
    Jul 7, 2023 at 7:15
  • 1
    $\begingroup$ Bypassing the validation to put something invalid in I don't think any of these approaches support in themselves, but if the concern is just being able to get a value into the location without the check recursing forever, a couple of points: the compiler can generate the checks right before every assignment throughout the program, rather than wrapping all access; the approach from First-Class Dynamic Types (paper here) intercepts during the assignment instead, so there's no recursion; any approach could allow an escape hatch if you want to design it in. $\endgroup$
    – Michael Homer
    Jul 7, 2023 at 7:21
  • 1
    $\begingroup$ That's weird, you mean the language may or may not eliminate dynamic validation for an input? Such an uncontrollable feature would be a disaster. I think it should refuse to compile unless the programmer explicitly assumes these conditions hold . $\endgroup$
    – Aster
    Jul 7, 2023 at 7:23
  • 1
    $\begingroup$ Anything that's mathematically provable is in scope for a theorem prover, but some properties are hard/too slow/undecidable-and-it-matters. I can't really put a boundary on which they are: even just numeric ranges can be difficult in many cases because of things like integer overflow. The search terms to find these systems will be "theorem prover" and "SMT solver", where SMT is "satisfiability modulo theories". $\endgroup$
    – Michael Homer
    Jul 7, 2023 at 7:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .