<p>I'm working on an experimental JVM-based programming language and would like record and verify additional type constraints (beyond the types themselves).
In Kotlin and many other modern programming languages you can write</p>
<pre><code>fun exp(base: Number, exponent: Int): Number
{
  return if (base is BigDecimal)
  {
    base.pow(exponent)
  }
  else 0
}
</code></pre>
<p>Even though <code>base</code> is declared as <code>Number</code> the compiler allows invoking the <code>pow</code> method, because at that location it is known that <code>base</code> is actually a <code>BigDecimal</code>. This is one of a few special cases where the compiler detects a particular situation and generates some extra code under the hood to make it work.</p>
<p>I would like to create a similar mechanism, but in a much more generic fashion, and I'd like to extend it from pure type information to also include additional predicates.
For example, division is only allowed when the divisor is non-zero, so I'd like to be able to extend this concept for cases like this:</p>
<pre><code>if (divisor != 0)
{
    dividend/divisor
}
</code></pre>
<p>The compiler should reject the division if it is not in a context where the divisor is known to be non-zero.
Notably, I would prefer as little as possible of the mechanism to be hard-coded into the compiler.
There is an existing syntax for expressing such type constraints:</p>
<pre><code>Real dividedBy[/](Real divisor:: != 0)
</code></pre>
<p>The method declaration indicates that the division can only be performed for non-zero divisors and should be flagged by the compiler otherwise.
Currently, the additional constraints are recorded as type annotations that are suitable for consumption by an SMT simplifier/solver (supporting a limited number of boolean and numeric operations).
However, I'm still struggling with collecting constraints in nested scenarios, and there are probably plenty of tricky scenarios that I don't even know about.</p>
<p>Are there existing languages that support such a mechanism that I could use as a template or guideline? Are there well-known implementation approaches for such a feature?</p>

<types><type-inference><type-checker><dependent-types>
Language that records and enforces type constraints/predicates
CC BY-SA 4.0
2024-09-01T23:13:50.613Z
I think these two previous questions are relevant here but likely not duplicates: [How the compiler or runtime handles types which are complex patterns or have complex constraints?](https://langdev.stackexchange.com/q/2146/133), [What language was the first to treat null checks as smart casts to non-nullable types?](https://langdev.stackexchange.com/q/3149/133)
Michael Homer
CC BY-SA 4.0
2024-09-01T23:17:28.933Z
Rust has a [NonZero](https://doc.rust-lang.org/std/num/struct.NonZero.html) type, but it's implemented in the library, not in the compiler, so it's not relevant here.
Eldritch Conundrum
CC BY-SA 4.0
2024-09-01T23:27:37.993Z
@EldritchConundrum Thanks, I'll still have a look at that Rust NonZero type. Ideally, I only want the compiler to provide the high-level mechanism, but specific constraints should be implementable in a library, etc. So, Rust's NonZero may not be all that far off.
raner
CC BY-SA 4.0
2024-09-03T13:07:21.883Z
As an aside, do you have more examples of constraints, appart from numerical constraints, subtyping contraints, and null?
Pablo H
CC BY-SA 4.0
2024-09-04T18:27:02.083Z
@PabloH You've pretty much summarized the main use cases in my mind. Size constraints on matrix and tensor types are another use that I'm interested in, but I guess that falls into the "numeric" category as well. Any boolean-valued function can be used in constraints, e.g., indicating whether the object has undergone a certain type of processing already. I see this feature mainly as a remedy for situations where purely type-based solutions run into problems with LSP or are otherwise unpractical (e.g., Integer and NonZeroInteger types), or where an existing API imposes sequential coupling.
raner
CC BY-SA 4.0
2024-09-06T05:21:15.863Z
For dynamic checks, it's called flow-sensitive typing. Check out [type narrowing in TypeScript](https://www.typescriptlang.org/docs/handbook/2/narrowing.html). More common in statically typed languages is refinement types. Every type can be refined with additional predicates, like your non-zero example. Check out [LiquidHaskell](https://ucsd-progsys.github.io/liquidhaskell/).
Jonathan Tran
CC BY-SA 4.0
2024-09-06T07:45:23.893Z
I think [Shen](https://shen-language.github.io/) might be interesting to know in this context, AFAIK the type system is using Prolog so its both powerful and undecidable
coredump
CC BY-SA 4.0
2024-10-25T08:56:25.377Z
C++ has `if constexpr (divisor != 0)` - not a special case at all. C++ compilers implement a fairly large subset of C++ at compile time. Also, C++ has first-class language support for _concepts_.
MSalters
<p>This looks like <a href="https://goto.ucsd.edu/%7Erjhala/liquid/liquid_types.pdf" rel="nofollow noreferrer">liquid types</a> (short for &quot;logically qualified data types&quot;), or more generally, refinement types.</p>
<p><a href="https://ucsd-progsys.github.io/liquidhaskell/" rel="nofollow noreferrer">Liquid Haskell</a> and <a href="https://fstar-lang.org/" rel="nofollow noreferrer">F*</a> support refinement types.</p>
<p>For example in F* you can write programs with statically-checked invariants like:</p>
<pre><code>let rec sorted_concat (#a:eqtype)
  (f:total_order_t a)
  (l1:list a{sorted f l1})
  (l2:list a{sorted f l2})
  (pivot:a)
  : Lemma (requires (forall y. mem y l1 ==&gt; not (f pivot y)) /\
  (forall y. mem y l2 ==&gt; f pivot y))
  (ensures sorted f (append l1 (pivot :: l2)))
</code></pre>

CC BY-SA 4.0
2024-10-25T07:12:36.007Z
2024-10-25T07:12:36.007Z
xuq01
CC BY-SA 4.0
2024-10-26T02:16:05.183Z
There is also [Flux](https://flux-rs.github.io/flux/): liquid types for Rust.
apropos
# Language that records and enforces type constraints/predicates
Posted by: username_0 on 2024-09-01
I'm working on an experimental JVM-based programming language and would like record and verify additional type constraints (beyond the types themselves).
In Kotlin and many other modern programming languages you can write
fun exp(base: Number, exponent: Int): Number
{
  return if (base is BigDecimal)
  {
    base.pow(exponent)
  }
  else 0
}

Even though base is declared as Number the compiler allows invoking the pow method, because at that location it is known that base is actually a BigDecimal. This is one of a few special cases where the compiler detects a particular situation and generates some extra code under the hood to make it work.
I would like to create a similar mechanism, but in a much more generic fashion, and I'd like to extend it from pure type information to also include additional predicates.
For example, division is only allowed when the divisor is non-zero, so I'd like to be able to extend this concept for cases like this:
if (divisor != 0)
{
    dividend/divisor
}

The compiler should reject the division if it is not in a context where the divisor is known to be non-zero.
Notably, I would prefer as little as possible of the mechanism to be hard-coded into the compiler.
There is an existing syntax for expressing such type constraints:
Real dividedBy[/](Real divisor:: != 0)

The method declaration indicates that the division can only be performed for non-zero divisors and should be flagged by the compiler otherwise.
Currently, the additional constraints are recorded as type annotations that are suitable for consumption by an SMT simplifier/solver (supporting a limited number of boolean and numeric operations).
However, I'm still struggling with collecting constraints in nested scenarios, and there are probably plenty of tricky scenarios that I don't even know about.
Are there existing languages that support such a mechanism that I could use as a template or guideline? Are there well-known implementation approaches for such a feature?
**Tags:** types type-inference type-checker dependent-types
> **Comments:**
> **username_1**: I think these two previous questions are relevant here but likely not duplicates: [How the compiler or runtime handles types which are complex patterns or have complex constraints?](https://langdev.stackexchange.com/q/2146/133), [What language was the first to treat null checks as smart casts to non-nullable types?](https://langdev.stackexchange.com/q/3149/133)  
> **username_2**: Rust has a [NonZero](https://doc.rust-lang.org/std/num/struct.NonZero.html) type, but it's implemented in the library, not in the compiler, so it's not relevant here.  
> **username_0**: @EldritchConundrum Thanks, I'll still have a look at that Rust NonZero type. Ideally, I only want the compiler to provide the high-level mechanism, but specific constraints should be implementable in a library, etc. So, Rust's NonZero may not be all that far off.  
> **username_3**: As an aside, do you have more examples of constraints, appart from numerical constraints, subtyping contraints, and null?  
> **username_0**: @PabloH You've pretty much summarized the main use cases in my mind. Size constraints on matrix and tensor types are another use that I'm interested in, but I guess that falls into the "numeric" category as well. Any boolean-valued function can be used in constraints, e.g., indicating whether the object has undergone a certain type of processing already. I see this feature mainly as a remedy for situations where purely type-based solutions run into problems with LSP or are otherwise unpractical (e.g., Integer and NonZeroInteger types), or where an existing API imposes sequential coupling.  
> **username_4**: For dynamic checks, it's called flow-sensitive typing. Check out [type narrowing in TypeScript](https://www.typescriptlang.org/docs/handbook/2/narrowing.html). More common in statically typed languages is refinement types. Every type can be refined with additional predicates, like your non-zero example. Check out [LiquidHaskell](https://ucsd-progsys.github.io/liquidhaskell/).  
> **username_5**: I think [Shen](https://shen-language.github.io/) might be interesting to know in this context, AFAIK the type system is using Prolog so its both powerful and undecidable  
> **username_6**: C++ has `if constexpr (divisor != 0)` - not a special case at all. C++ compilers implement a fairly large subset of C++ at compile time. Also, C++ has first-class language support for _concepts_.  
---
## 1 answers
### Answer by username_7 on 2024-10-25. Score: 2
This looks like liquid types (short for "logically qualified data types"), or more generally, refinement types.
Liquid Haskell and F* support refinement types.
For example in F* you can write programs with statically-checked invariants like:
let rec sorted_concat (#a:eqtype)
  (f:total_order_t a)
  (l1:list a{sorted f l1})
  (l2:list a{sorted f l2})
  (pivot:a)
  : Lemma (requires (forall y. mem y l1 ==> not (f pivot y)) /\
  (forall y. mem y l2 ==> f pivot y))
  (ensures sorted f (append l1 (pivot :: l2)))
> **Comments:**
> **username_8** (2024-10-26): There is also [Flux](https://flux-rs.github.io/flux/): liquid types for Rust.  
---
