<h2>Pattern Types</h2>
<p>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:</p>
<pre><code>class UserData &lt; 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
</code></pre>
<p>To me, you should be able to do this, and so there is no difference between a &quot;validation&quot; and a &quot;type check&quot;:</p>
<pre><code>if (isString(val)) {
  log('is string!')
}

if (isEmail(val)) {
  log('is email!')
}
</code></pre>
<p>The reason why <code>isEmail</code> isn't traditionally considered in the realm of <em>typechecking</em> 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 <a href="https://stackoverflow.com/a/9374698/169992">here</a> (I don't see how this could be done at compile time in any case, it seems like it should be done at runtime):</p>
<pre><code>type BoundedInt(n) = {i:Int | i&lt;=n}

# dependent type used
def min(i : Int, j : Int) : BoundedInt(j) =
  if i &lt; j then i else j
</code></pre>
<p>You might have something like:</p>
<pre><code>type Email(x) = {x:String and x.match(/regex/)}

def login(email: Email) =
  # do login
</code></pre>
<p>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 <em>other</em> than at runtime.</p>
<pre><code>let val = readFile('./foo.txt')
login(val) # what happens here?
</code></pre>
<p>So that is my part about pattern types (regexp being string patterns, but perhaps there are other patterns too).</p>
<h2>Constraint Types</h2>
<p>A &quot;constraint type&quot; 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).</p>
<pre><code>type Color = {
  r: BoundedInt(256),
  g: BoundedInt(256),
  b: BoundedInt(256),
}

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

type SomethingRandom = {
  a: Int
  b: Int
} where (self) {
  if (self.a &gt; 100) {
    assert self.b === 12
  } else if (self.a &gt; 10) {
    assert self.b === 32
  } else if (self.a === 4) {
    assert self.b === 42
  }
}
</code></pre>
<p>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?</p>
<h2>Conclusion</h2>
<p>Even if they can't be done at compile-time, and only can be done at runtime, <strong>couldn't we still call them &quot;types&quot;</strong>? Why do we consider <code>String</code> a type, but <code>Email</code> 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.</p>
<p>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?</p>

<types><type-checker>
How the compiler or runtime handles types which are complex patterns or have complex constraints?
CC BY-SA 4.0
2023-07-07T06:09:39.893Z
Yes. These are called refinement types.
pxeger
CC BY-SA 4.0
2023-07-07T06:10:48.143Z
@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).
Lance Pollard
CC BY-SA 4.0
2023-07-07T06:11:42.827Z
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.
Aster
CC BY-SA 4.0
2023-07-07T06:43:38.697Z
@Aster how is that possible with `let email = readFile('./foo.txt'); login(email)`?
Lance Pollard
CC BY-SA 4.0
2023-07-07T07:04:08.120Z
```
Email :: String<\x -> is_email x>
Login :: String -> IO Email
```
Aster
CC BY-SA 4.0
2023-07-07T07:57:35.367Z
@Aster I still don't see how that can hold at compile time.
Lance Pollard
<p>You can still call them types, and languages do. You've referred to dependent types already, but <em>refinement types</em> 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.</p>
<p>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. <a href="https://en.wikipedia.org/wiki/Whiley_(programming_language)" rel="noreferrer">Whiley</a> is one language that does this while otherwise behaving like an ordinary programming language. It permits type definitions</p>
<pre class="lang-none prettyprint-override"><code>type ArrayOfPositive is (int[] items) where all { i in 0..|items| | items[i] &gt; 0 }
type pos is (int p) where p &gt; 0
</code></pre>
<p>and it won't allow any non-positive value into an <code>ArrayOfPositive</code>, but will allow any value out of it to go into a <code>pos</code>-typed variable.</p>
<p><code>pos n = 3</code> will work, and <code>pos n = -2</code> will not work, statically; a loop that counts down in a <code>pos</code> 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 <code>i</code> is positive, you're now allowed to put it into one of those arrays.</p>
<p>Building a theorem prover into your type checker is enough of a thing for that to be <em>the</em> 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.</p>
<hr />
<p>Other languages allow similar things with only run-time checking. <a href="https://docs.raku.org/language/typesystem#subset" rel="noreferrer">Raku is one of these</a>:</p>
<pre class="lang-none prettyprint-override"><code>subset Positive of Int where * &gt; 0;
</code></pre>
<p>defines a type <code>Positive</code> that only holds positive integers.</p>
<p>Raku permits some fairly extreme cases in the <code>where</code> clause, including something like <code>subset F of Str where *.IO.f</code>, which is <strong>the type of names of existing files</strong>, which can't possibly be validated at compile time. Given a declaration <code>my F $x</code>, 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.</p>
<p>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.</p>
<hr />
<p>It's also possible to allow arbitrary checker objects to be elevated to use as &quot;types&quot;. This is the approach in <a href="https://doi.org/10.1145/3359619.3359740" rel="noreferrer">First-Class Dynamic Types</a> (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 <em>at run time</em>, 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 &quot;types&quot;, but it's essentially fair enough when they perform the same dynamic validation as any sound gradual type checker would.</p>
<p>If you want to allow any constraint at all to be representable as a named &quot;type&quot; 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 &quot;type&quot;, but directing the code into different implementations based on matching, or erroring out — so that you could have one &quot;login&quot; 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 <a href="https://langdev.stackexchange.com/q/1802/133">not highly common</a> you do see them in quite a few languages.</p>

CC BY-SA 4.0
2023-07-07T06:58:03.197Z
2023-07-07T06:58:03.197Z
Michael Homer
CC BY-SA 4.0
2023-07-07T07:10:40.913Z
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).
Lance Pollard
CC BY-SA 4.0
2023-07-07T07:14:30.320Z
Oh also, for doing things like runtime checks that a string matches a regex, does that mean the compiler inserts code and that it wraps the actual property with a getter/setter (sort of like Rails attributes)? In that case, I'm wondering how/if you could bypass these validations (like you can in Rails), or otherwise set the prop directly, rather than going through the "validated" accessors.
Lance Pollard
CC BY-SA 4.0
2023-07-07T07:15:16.113Z
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.
Michael Homer
CC BY-SA 4.0
2023-07-07T07:21:05.313Z
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](https://mwh.nz/pubs/dls2019)) intercepts *during* the assignment instead, so there's no recursion; any approach could allow an escape hatch if you want to design it in.
Michael Homer
CC BY-SA 4.0
2023-07-07T07:23:04.283Z
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 .
Aster
CC BY-SA 4.0
2023-07-07T07:24:28.763Z
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".
Michael Homer
CC BY-SA 4.0
2023-07-07T07:27:01.103Z
@Aster Maybe? Falling back to dynamic checks isn't ideal, but if you want to ensure that certain code doesn't run when a property doesn't hold, bailing out at run time is better than letting it happen, and if the property you wanted was beyond what it's possible to check statically... I would at least want to be warned about it and able to choose rejection, personally. It does depend on what level of guarantee you want, and I can see reasonable cases for this, just like gradual typing.
Michael Homer
CC BY-SA 4.0
2023-07-07T07:27:06.897Z
Excellent, yeah there is no need for validation escape hatch, was just curious.
Lance Pollard
CC BY-SA 4.0
2023-07-07T07:29:25.387Z
@MichaelHomer when you say "falling back to dynamic checks isn't ideal", isn't that a misnomer? Falling back to dynamic checks if _required_ in many many cases it seems, even like you're saying in numeric ranges which can be difficult (but is a super basic case of these kinds of types). But the ideal would be to first try and find a way to do static checks. I think that's what you're basically saying, but correct me if I'm wrong.
Lance Pollard
CC BY-SA 4.0
2023-07-07T07:36:35.057Z
@Lance Aster's position (I think) is that if you couldn't guarantee your correctness property statically, your program isn't known to be correct and you should reject it until it is (that is, a "maybe" is a "no"). This is a pretty reasonable position if you're relying on those guarantees: consider a type checker that allows all downcasts because they *might* work at run time, and just crashes when they're wrong - we'd say that was bad. For some other properties static checking is never possible, and you're always in dynamic-land, so that's what you expected. It's not always desirable, though.
Michael Homer
# How the compiler or runtime handles types which are complex patterns or have complex constraints?
Posted by: username_0 on 2023-07-07
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?
**Tags:** types type-checker
> **Comments:**
> **username_1**: Yes. These are called refinement types.  
> **username_0**: @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).  
> **username_2**: 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.  
> **username_0**: @Aster how is that possible with `let email = readFile('./foo.txt'); login(email)`?  
> **username_2**: ```
Email :: String<\x -> is_email x>
Login :: String -> IO Email
```  
> **username_0**: @Aster I still don't see how that can hold at compile time.  
---
## 1 answers
### Answer by username_3 on 2023-07-07. Score: 6 | Accepted answer
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.
> **Comments:**
> **username_0** (2023-07-07): 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).  
> **username_0** (2023-07-07): Oh also, for doing things like runtime checks that a string matches a regex, does that mean the compiler inserts code and that it wraps the actual property with a getter/setter (sort of like Rails attributes)? In that case, I'm wondering how/if you could bypass these validations (like you can in Rails), or otherwise set the prop directly, rather than going through the "validated" accessors.  
> **username_3** (2023-07-07): 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.  
> **username_3** (2023-07-07): 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](https://mwh.nz/pubs/dls2019)) intercepts *during* the assignment instead, so there's no recursion; any approach could allow an escape hatch if you want to design it in.  
> **username_2** (2023-07-07): 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 .  
> **username_3** (2023-07-07): 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".  
> **username_3** (2023-07-07): @Aster Maybe? Falling back to dynamic checks isn't ideal, but if you want to ensure that certain code doesn't run when a property doesn't hold, bailing out at run time is better than letting it happen, and if the property you wanted was beyond what it's possible to check statically... I would at least want to be warned about it and able to choose rejection, personally. It does depend on what level of guarantee you want, and I can see reasonable cases for this, just like gradual typing.  
> **username_0** (2023-07-07): Excellent, yeah there is no need for validation escape hatch, was just curious.  
> **username_0** (2023-07-07): @MichaelHomer when you say "falling back to dynamic checks isn't ideal", isn't that a misnomer? Falling back to dynamic checks if _required_ in many many cases it seems, even like you're saying in numeric ranges which can be difficult (but is a super basic case of these kinds of types). But the ideal would be to first try and find a way to do static checks. I think that's what you're basically saying, but correct me if I'm wrong.  
> **username_3** (2023-07-07): @Lance Aster's position (I think) is that if you couldn't guarantee your correctness property statically, your program isn't known to be correct and you should reject it until it is (that is, a "maybe" is a "no"). This is a pretty reasonable position if you're relying on those guarantees: consider a type checker that allows all downcasts because they *might* work at run time, and just crashes when they're wrong - we'd say that was bad. For some other properties static checking is never possible, and you're always in dynamic-land, so that's what you expected. It's not always desirable, though.  
---
