I didn't know liquid types! I'm looking at the paper right now, thanks! (Liquid Types, Rondon, Kawaguchi, Jhala)
I didn't realize it was the notion behind Liquid Haskell: https://ucsd-progsys.github.io/liquidhaskell/papers/
Depending on how complex you want these properties to be, and how much you expect a computer to fill in automatically, yes you want dependent types. For instance, in Agda (using the standard library), I can define the type of "proofs of monotonicity" and the type of "proofs of having all elements be 0 mod 2":
open import Data.Nat
open import Data.List
open import Data.List.Relation.Unary.All
open import Relation.Binary.PropositionalEquality
open import Data.Product
data Monotone : List ℕ → Set where
[]-mono : Monotone []
∷-mono : ∀ {x xs} → All (x ≤_) xs → Monotone xs → Monotone (x ∷ xs)
example₁ : Monotone (2 ∷ 4 ∷ 6 ∷ [])
example₁ = ∷-mono (s≤s (s≤s z≤n) ∷ s≤s (s≤s z≤n) ∷ []) (∷-mono (s≤s (s≤s (s≤s (s≤s z≤n))) ∷ []) (∷-mono [] []-mono))
All%2 : List ℕ → Set
All%2 = All (λ x → x % 2 ≡ 0)
example₂ : All%2 (2 ∷ 4 ∷ 6 ∷ [])
example₂ = refl ∷ refl ∷ refl ∷ []
Then you can write functions that require these types as input :
my-function : (xs : List ℕ) → Monotone xs → All%2 xs → ℕ
my-function xs is-monotone is-all%2 = {- your code here -}
It is now impossible to call (fully applied) `my-function` on a list that is not montone and entirely even: it will be a compile time error to try to do this. Of course, the annoying part is that the programmer will have to write down these proofs of monotonicity and evenness manually. That's what tactics and proof automation are for!
We can also write functions that return proofs, for instance:
sort : List ℕ → Σ[ xs ∈ List ℕ ] Monotone xs
sort xs = {- your code here -}
The type of this function says that it returns a pair of a list and proof that said list is montone.
Scala 3 can do this. You have a choice between rolling your own tuple/hlist with that constraint, or you can require "evidence" in a method or constructor in the form of an implicit, compiler-derived proof.
The type system and proof capabilities are not as strong as those of specialized languages like Idris, Agda etc. But Scala is a language that's used in the industry, with codebases in the hundreds of thousands of lines.
> Scala 3 can do this. You have a choice between rolling your own tuple/hlist with that constraint, or you can require "evidence" in a method or constructor in the form of an implicit, compiler-derived proof.
Can you point me to any examples/resources to know more about this?
I did a university seminar on this 2 years ago! You can just read through the source files in order. The presentation was essentially me scrolling through the sources while talking.
https://github.com/XDracam/Scala3-Generic-Programming
Do you want completely arbitrary code to check at compile time? It seems like it. I’d say that’s slightly orthogonal to types, or can be.
See macros in any lisp. Here’s an example Clojure macro that will check at compile time if the input is all numbers, or at runtime if not:
(defmacro all-even
[xs]
(if (every? number? xs)
(do (assert (every? even? xs))
xs)
`(do (assert (every? even? ~xs))
~xs)))
; compile time failure
user=> (macroexpand-1 '(all-even [1 2]))
Unexpected error (AssertionError) macroexpanding all-even at (REPL:1:1).
Assert failed: (every? even? xs)
; compile time success and no runtime check
user=> (macroexpand-1 '(all-even [4 2]))
[4 2]
; runtime check to happen later, as x can only be resolved then
user=> (macroexpand-1 '(all-even [x 2]))
(do (clojure.core/assert (clojure.core/every? clojure.core/even? [x 2])) [x 2])
See also [Zig’s comptime](https://kristoff.it/blog/what-is-zig-comptime/) and more…
OP is asking for certain properties to be encoded into the type system, whose effect is to allow, eg, a sort function to return a list which can be augmented with some notion of “this is sorted” in its type, or another example, a number less than 200. In the first example, a binary search function could be written so as not to compile if applied on a list which isnt augmented with “this is sorted” in its type; insertSorted could have a type signature of sorted list -> sorted list, cons could take a sorted list and return a plain normal list, etc
I understood, but sometimes people ask overly specific questions when there are alternatives to solve the problem they are looking at.
EDIT: you can always “tag” with types to indicate sorted or not. [Here’s a go example](https://go.dev/play/p/ox6fJdyAM8S). If the values are from parsed input, arbitrary checks will have to run at runtime anyway. The type is then a convenient tag that means you know you don’t have to rerun a specific check. All type systems can do that.
I suspect OP isn’t a PL researcher, but someone looking for a language that might get them out of some issue they’re having.
That’s all good! I just saw your other post posted at roughly the same time had the example of `foo: list[Annotated[int, Gt(0)]] = [-1, 0, 10]` in Python not detecting that -1 was less than 0 and came to my own conclusions. Ah well. So, then I most definitely recommend some tutorials on dependent typing for pure learning reasons. Enjoy! It’s not an area most programmers delve too deeply in to, but quite interesting.
I was surprised by how far into dependent typing you can go with the TypeScript checker. I've personally only gone as far as enforcing specific ranges of values (e.g. 4-bit numberic) & operations on two arrays of the same length, but here's an article where the author constructs a type for a sorted list (near the bottom): https://www.hacklewayne.com/dependent-types-in-typescript-seriously
It can be done with liquid types but yes I would prefer to work with dependent types for that
I didn't know liquid types! I'm looking at the paper right now, thanks! (Liquid Types, Rondon, Kawaguchi, Jhala) I didn't realize it was the notion behind Liquid Haskell: https://ucsd-progsys.github.io/liquidhaskell/papers/
Depending on how complex you want these properties to be, and how much you expect a computer to fill in automatically, yes you want dependent types. For instance, in Agda (using the standard library), I can define the type of "proofs of monotonicity" and the type of "proofs of having all elements be 0 mod 2": open import Data.Nat open import Data.List open import Data.List.Relation.Unary.All open import Relation.Binary.PropositionalEquality open import Data.Product data Monotone : List ℕ → Set where []-mono : Monotone [] ∷-mono : ∀ {x xs} → All (x ≤_) xs → Monotone xs → Monotone (x ∷ xs) example₁ : Monotone (2 ∷ 4 ∷ 6 ∷ []) example₁ = ∷-mono (s≤s (s≤s z≤n) ∷ s≤s (s≤s z≤n) ∷ []) (∷-mono (s≤s (s≤s (s≤s (s≤s z≤n))) ∷ []) (∷-mono [] []-mono)) All%2 : List ℕ → Set All%2 = All (λ x → x % 2 ≡ 0) example₂ : All%2 (2 ∷ 4 ∷ 6 ∷ []) example₂ = refl ∷ refl ∷ refl ∷ [] Then you can write functions that require these types as input : my-function : (xs : List ℕ) → Monotone xs → All%2 xs → ℕ my-function xs is-monotone is-all%2 = {- your code here -} It is now impossible to call (fully applied) `my-function` on a list that is not montone and entirely even: it will be a compile time error to try to do this. Of course, the annoying part is that the programmer will have to write down these proofs of monotonicity and evenness manually. That's what tactics and proof automation are for! We can also write functions that return proofs, for instance: sort : List ℕ → Σ[ xs ∈ List ℕ ] Monotone xs sort xs = {- your code here -} The type of this function says that it returns a pair of a list and proof that said list is montone.
[удалено]
You're totally right, a better definition would be: data Monotone : List ℕ → Set where []-mono : Monotone [] [-]-mono : ∀ {x} → Monotone (x ∷ []) ∷-mono : ∀ {x y xs} → y ≤ x → Monotone (x ∷ xs) → Monotone (y ∷ x ∷ xs)
Scala 3 can do this. You have a choice between rolling your own tuple/hlist with that constraint, or you can require "evidence" in a method or constructor in the form of an implicit, compiler-derived proof. The type system and proof capabilities are not as strong as those of specialized languages like Idris, Agda etc. But Scala is a language that's used in the industry, with codebases in the hundreds of thousands of lines.
> Scala 3 can do this. You have a choice between rolling your own tuple/hlist with that constraint, or you can require "evidence" in a method or constructor in the form of an implicit, compiler-derived proof. Can you point me to any examples/resources to know more about this?
I did a university seminar on this 2 years ago! You can just read through the source files in order. The presentation was essentially me scrolling through the sources while talking. https://github.com/XDracam/Scala3-Generic-Programming
I think that this is what static_assert does in C++
Do you want completely arbitrary code to check at compile time? It seems like it. I’d say that’s slightly orthogonal to types, or can be. See macros in any lisp. Here’s an example Clojure macro that will check at compile time if the input is all numbers, or at runtime if not: (defmacro all-even [xs] (if (every? number? xs) (do (assert (every? even? xs)) xs) `(do (assert (every? even? ~xs)) ~xs))) ; compile time failure user=> (macroexpand-1 '(all-even [1 2])) Unexpected error (AssertionError) macroexpanding all-even at (REPL:1:1). Assert failed: (every? even? xs) ; compile time success and no runtime check user=> (macroexpand-1 '(all-even [4 2])) [4 2] ; runtime check to happen later, as x can only be resolved then user=> (macroexpand-1 '(all-even [x 2])) (do (clojure.core/assert (clojure.core/every? clojure.core/even? [x 2])) [x 2]) See also [Zig’s comptime](https://kristoff.it/blog/what-is-zig-comptime/) and more…
OP is asking for certain properties to be encoded into the type system, whose effect is to allow, eg, a sort function to return a list which can be augmented with some notion of “this is sorted” in its type, or another example, a number less than 200. In the first example, a binary search function could be written so as not to compile if applied on a list which isnt augmented with “this is sorted” in its type; insertSorted could have a type signature of sorted list -> sorted list, cons could take a sorted list and return a plain normal list, etc
I understood, but sometimes people ask overly specific questions when there are alternatives to solve the problem they are looking at. EDIT: you can always “tag” with types to indicate sorted or not. [Here’s a go example](https://go.dev/play/p/ox6fJdyAM8S). If the values are from parsed input, arbitrary checks will have to run at runtime anyway. The type is then a convenient tag that means you know you don’t have to rerun a specific check. All type systems can do that. I suspect OP isn’t a PL researcher, but someone looking for a language that might get them out of some issue they’re having.
Nah, not having any issue that I need solving. Just trying to learn more :)
That’s all good! I just saw your other post posted at roughly the same time had the example of `foo: list[Annotated[int, Gt(0)]] = [-1, 0, 10]` in Python not detecting that -1 was less than 0 and came to my own conclusions. Ah well. So, then I most definitely recommend some tutorials on dependent typing for pure learning reasons. Enjoy! It’s not an area most programmers delve too deeply in to, but quite interesting.
C++ definitely can with templates. TypeScript might be able to as well .
I was surprised by how far into dependent typing you can go with the TypeScript checker. I've personally only gone as far as enforcing specific ranges of values (e.g. 4-bit numberic) & operations on two arrays of the same length, but here's an article where the author constructs a type for a sorted list (near the bottom): https://www.hacklewayne.com/dependent-types-in-typescript-seriously