Idris 2: Quantitative Type Theory in Practice
arxiv.org
arxiv.org
I'm a phd student working on Idris and I used to work with Edwin on this, if you want more info or want to see more practical applications of idris2, Dependent types, or QTT, here are a couple links:
- idris2 is written in idris2 so that's a good example of a big program using dependent types https://github.com/idris-lang/Idris2
- we have some very interesting libraries in the works: https://github.com/idris-lang/Idris2/wiki/Libraries
- my own projects in idris include a purely declarative server library where you give the API and the server is completely implemented and instantiated from your description https://gitlab.com/avidela/recombine
It's currently one of my project to use QTT to statically enforce performance invariants and optimisations, currently I am looking at partial evaluation of programs and explicit annotations to control which parts need to be partially evaluated and which parts need to remain Unevaluated.
Regarding the benchmarks there are two things to address to make them go faster:
- the idris parser is actually pretty slow so we should get working on that
- the examples use explicit runtime bindings for type parameters which force the types to be allocated and available at runtime, which destroys the performance of some programs (stlc notably)
It's not expected to write idris code in that way since linearity annotations also allow you to _remove_ values from the runtime and make dependent programs go faster, if you were to be concerned about runtime performance you would use _runtime erased_ type variables instead of _runtime relevant_ variables. Some of this is due to the foreign nature of QTT, and we should do a better job at teaching how to use it for performance.
On the other hand someone could argue "if idris is that smart can't it warn/perform those optimisations automatically?" And maybe that's the way to go, but we need more eyes and brain looking at the problem and coming up with prototype solutions to make progress. idris is still a small project so we don't have enough people working on it to implement those smart features
Technically speaking multiplicity 1 (linear variable) can be subject to arbitrary inclining though it's not implemented in the compiler.
I'm working on other multiplicities that could allow you to describe which values are "compile-time" available, and therefore subject to optimisations
Does this apply even for compile-time evaluation? I'm not sure of the specifics of how Idris does compile-time evaluation vs runtime evaluation.
- idris is written in idris so any improvement in the language results in faster compile-times, if more things are annotated with 0 in the compiler, thing will compile faster.
- if some variable is only important at compile-time, the compiler doesn't have to look at it with very much scrutiny. That saves you a lot of time when typechecking
Right, but if some code is annotated with unrestricted multiplicity, but still not actually used anywhere in a function body, does this make compilation of that code slower than if that same code was annotated with zero multiplicity?
However, it's still based on Idris 1 (which didn't have QTT). The basics haven't changed much though (some examples have to be modified slightly, mostly related to making some arguments explicit that used to be implicit).
Idris seems like a really interesting language. Examples from the book include:
- typesafe printf (it will check that the correct number of arguments with the correct types are passed at compile time).
- proving that functions are total (roughly that means that they terminate for every input)
- writing infinitely running programs as a stream of actions, meaning that the majority of the program can be written as a total function and only the top-level function actually consuming the actions needs to be partial
- views with dependent pattern matching for traversing structures safely in several ways
- safe division
- ability to define all the effects your system uses instead of using an unrestricted IO type
etc.
While the examples are super interesting I don't think that I yet fully grasp all the possible things you could do with dependent types (or what sorts of limitations they have). I guess that would come with more practice.
For example, it seems like Idris doesn't really support subtyping unless I've missed something obvious (you can use typeclasses, but that doesn't allow you to use heterogeneous collections or anything). I believe it's also a requirement that all functions used in type signatures are total.
Yes of course. All languages have specific syntax and semantics. That doesn’t change the fact that you can encode all of math in it which is a huge deal. It allows you to prove code correct (see CompCert, seL4, CertOS etc.)
And yes you can’t prove anything unless the functions you use are total. That’s a basic requirement for any language where you want to use the type system to prove correct code. Allowing non-total functions would allow you to prove false. And you can prove anything you want from false.
But in terms of practical developments, these "restrictions" can matter. Especially when you have specific maintenance concerns. And I'm talking more about programming than theorem proving (Idris is, after all, more geared towards the former than the latter unlike e.g. Coq or Lean).
I've had a problem in the back of my head for a while and I knew it would probably be a bit cumbersome to do in Haskell (although maybe with some advanced extensions it's possible?). I thought that dependent types might solve that problem but I yet don't see a way how I could do that, at least in Idris (possibly I'm missing out on some very obvious way). I think I'd really need subtyping to make it work in a non-cumbersome way. (Or else, possibly some code generation for the boilerplate part.)
The context is a mathematical problem solver. Mathematical terms form hierarchies (possibly not a single one), and certain operations only make sense for certain types of terms (e.g. inverting a matrix), while others apply to all terms (e.g. simplifying an expression). I want to be able to verify this at compile time and at the same time, the function signatures should be "easy" enough that operations can be composed through operators (i.e. manually passing proof terms probably wouldn't work as well).
In a language like Haskell, I could probably use wrapper types, e.g.
data Matrix = ...
data Integral = ...
...
data Term = MatrixT Matrix | IntegralT Integral | ...
I'm thinking that in Idris, maybe I could do something like:
data TermType = MatrixT Nat Nat a | IntegralT | ...
data Term : TermType -> Type where
Matrix : Vect n (Vect m a) -> Term (MatrixT n m a)
Integral : Term -> Term Integral T
This is all based on work that I previously did, but where all these checks did unfortunately not happen at compile time, so every operation needed to have explicit runtime type checks (this was in a language with subtyping though).
The example given in the paper is a LinArray (https://github.com/idris-lang/Idris2/blob/main/libs/contrib/...). Unfortunately, as the community discovered, a user can "leak" a non-linear binding outside of the `newArray` constructor (which is what attempts to enforce linearity for all bindings). With multiple unrestricted handles, a user can accidentally double-free for instance. (https://github.com/idris-lang/Idris2/issues/613)
The fundamental issue in this case is that linearity in QTT is a property of the parameter bindings and _not_ the type itself, meaning we can't easily express linearity as a _global_ property of the type.
On the other hand, only affecting the parameter bindings makes it really easy to use runtime-erased/comptime stuff without reimplementing a bunch of common types as runtime- and comptime-only versions.
ATS chooses the other path and makes linearity and runtime-erasure a part of the type (not without paying a hefty syntactic cost however).
So I'm a bit confused why e.g. `read` is `(1 _ : arr t) -> Int -> Maybe t` and not `(1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))`.
But also isn't the `newArray` fixed by just rewrapping the output?
data Unrestricted : Type -> Type where
MkUnrestricted : a -> Unrestricted a
newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> Unrestricted a) -> Unrestricted a
-- You'll need this if you actually make use of the outer linear multiplicity
-- in the function argument to newArray
-- which is also why newArray returns Unrestricted
useUnrestricted : (1 _ : Unrestricted a) -> (a -> b) -> b
useUnrestricted (MkUnrestricted x) f = f x
The entire `Data.Linear.Array` seems to be in need of a once-over unless I'm misunderstanding something.
EDIT: Never mind, reading too quickly, I see the mread now that has the signature I'd imagine it should.
Linear types lets you do things like "this data can only be written to a file once".
It gives the example of a key in a database, which can return multiple types of values:
type DB = (k: Key) => Option[k.Value]
trait Key { type Value }
https://docs.scala-lang.org/scala3/book/types-dependent-func...
interface Key<V> { ... }
class Name extends Key<String> { ... }
class Age extends Key<Integer> { ... }
interface DB {
public <V> Optional<V> get(Key<V> k) { ... }
} Name nameKey = ...;
Age ageKey = ...;
Optional<String> name = db.get(nameKey);
Optional<Integer> age = db.get(ageKey);Optional<1> and Optional<“Name”>. You can only have types as arguments.
C++ has some dependent types in it allows you to have generic arguments be ints std::array<…, 4> but it still does not allow most values as generic type argument.
Here's an example that extends it slightly and can't be emulated by Java.
// I forget if I need to curry the second argument in a separate argument list
// I'm not next to a computer with scalac at the moment, so I'll just use separate argument lists
type DB = (k: Key) => k.IsVerified => Option[k.Value]
trait Key {
type Value
val keyValue: Value
case class IsVerified(underlyingBool: Boolean)
}
val myDB: DB =
key => isVerified => x match
case IsVerified(bool) =>
if bool then
// return the actual value
doSomething()
else
None
def verifyKey(key: Key): key.IsVerified =
if isValidKey(key) then
key.IsVerified(true)
else
key.IsVerified(false)
val key0: Key = ...
val key1: Key = ...
val key0Verification: key0.IsVerified = verifyKey(key0)
// Fails to compile
// You're trying to cheat!
// You only verified key0 and are trying to use its verification to bypass
// verifying key1
myDB(key1)(key0Verification)In theory you can do this kind of thing in Java, but you have to give each key its own type (cumbersome because Java doesn't have singleton types) and carry the type parameters arbitrarily far back through the call graph. E.g. imagine writing a function that appends 3 type-length vectors together - in a dependently-typed language you write this as:
def append[T, M, N, L](first: Vec[T, M], second: Vec[T, N], third: Vec[T, L]): Vec[T, M + N + L] = ...
<T, M, N, L, P, R> Vec<T, P> append (first: Vec<T, M>, second: Vec<T, N>, third: Vec<T, L>, isSum1: IsSum<M, N, P>, isSum2: IsSum<P, L, R>) { ... }
This isn't really the thing that dependent types provide though. If you have type-level computation without dependent types that's enough to avoid this problem (and e.g. Scala has this). However, dependent types are when the `+` in your first append is the same `+` as the usual runtime `+` rather than a separate type-level function that only works with types, not runtime values. Scala does not have this. Its dependent types are much more limited.
app : Vect n a -> Vect m a -> Vect (n + m) a
[1] Taken from https://www.idris-lang.org/pages/example.html
Scala has only a very limited version of dependent types. Even its "dependent function types" are a more restricted version of general dependent function types. Full dependent types can in a certain sense be even simpler than non-dependently-typed languages (e.g. you no longer need a separate notion of generics).
My understanding of "Linear Types" is that they are geared towards declaring values/types that can be used only once.
If this sounds weird, I thought so too. Except it turns out there a number of (fairly common) scenarios in which you might want to ensure that a value is only possible to be used once.
I've drank too much so I can't conjure many to mind, but what I can think of is something like a buffer in a lexer, where you want to ensure that a token is consumed once and then not available.
There are some decent examples in the Tweag repo for the GHC Linear Types proposal:
The OP has some examples. One of them is creating verified state machines (i.e. stating invariants that different states and transitions should obey all the way up to entirely specifying the abstract state machine). The paper uses linear types to replace Idris 1's ST type. Another is enforcing order of messages to be sent in a bidirectional communication protocol. There's also a lot more low-level examples (make sure that files get closed after use, make sure mutable variables are used correctly, etc.).
In general invariants of the form "verify that this happens after that happens" (and note that this phrase has two meanings which both are covered, verify that e.g. a clean up action always occurs when an action that requires clean up has happened and also verify that e.g. an action occurs after another action, and not before) can be enforced by linear types, which covers a large amount of what happens with stateful computing.
It would actually solve a lot of issues in Rust, but unfortunately would be an insane amount of work to introduce because they would invade a lot of the current type system
A good practical description of linear logic (but not types) is here: https://hashingit.com/elements/research-resources/1994-03-Fo...
Yes it's about how Forth implements linear logic without realizing it ;).
I don't think that's a particularly enlightening example, mostly because we can implement such a function without any linear or dependent types.
Consider that a list (of some element type T) could contain zero Ts, or one T, or two Ts, etc. i.e.
List<T> = 1 + T + (T × T) + (T × T × T) + ...
- `1` is a type containing only one value, like 'Unit', 'Null', 'Nil, etc. We use this to represent the empty list.
- 'X + Y' is the (tagged) union of types X and Y; AKA a sum type, or an Either
- 'X × Y' is the type of tuples containing an X and a Y; AKA a product type, or a Pair
Non-empty lists are almost the same, except we don't want to allow the empty list. Hence we need to get rid of the '1' type, to get something like this:
NonEmptyList<T> = T + (T × T) + (T × T × T) + ...
NonEmptyList<T> = T + (T × T) + (T × T × T) + (T × T × T × T) + ...
= (T × 1) + (T × T) + (T × T × T) + (T × T × T × T) + ...
= T × ( 1 + T + ( T × T) + ( T × T × T) + ...)
= T × List<T>
Note that we can go the other way too, if our language provided non-empty lists and we want to allow empty ones too:
List<T> = 1 + T + (T × T) + (T × T × T) + ...
= 1 + NonEmptyList<T>
Maybe<T> = 1 + T
List<T> = Maybe<NonEmptyList<T>>That alone is worth it imho.
In the run length encoding example, I don’t understand how the runtime data structure is defined. There is a Runlength data type, but its definition looks more like a Haskell-style curried function definition than a data definition. It seems to call the ‘rep’ function and the list concatenation operator, but how do you get a datatype out of that? If you drew a boxes and arrows diagram showing how the data is stored, what would it look like?
I’m wondering if this is like how you can use a closure to store data in captured local variables? Or perhaps like lazy evaluation in Haskell?
The RunLength data type is built such as if you give it a list, it gives you a (unique) type.
And the only two constructors available are such that they enforce the encoding.
Try to unroll an example or build one from the definition and you’ll get it eg.:
How would you build an element of this type?
RunLength [1 1 1 3 3 7 7 7]The input parameters to the "functions" appear to be data elements from within the compressed list. Because that's what they are. But this wasn't obvious to me.
I think the weird bit is when the tags and fields within a datatype are represented using the same syntax as a function's name and parameters. This punning threw me off. I suppose the same is true in Haskell, but you don't write type constructors using '->' between the fields, so this punning is less obvious. (And Haskell's syntax for product types is itself less familiar to me than a 'struct' definition in a C-like language.)
That's exactly how you write GADTs in Haskell: https://downloads.haskell.org/~ghc/6.6/docs/html/users_guide....
> how the data is stored
Thinking of how concretely the data is stored is a little bit tricky. I find it easier to build an intuition by looking at what kind of values the type signature lets us build, and which values are disallowed.
runLengthOfAnEmptyList : RunLength []
runLengthOfAnEmptyList = Empty
-- Note that 1 is shorthand for (S Z)
runLengthOfAListWithOneElement : RunLength [ 1 ]
runLengthOfAListWithOneElement = Run 0 1 Empty
-- The definition of RunLength places restrictions on how to
-- construct it.
-- For example, this will not compile.
runLengthOfAListWithOneElementBrokenVersion : RunLength [ 1 ]
runLengthOfAListWithOneElementBrokenVersion = Run 1 1 Empty
--
-- This violates the type signature of RunLength
-- Notice Run 1 1 Empty which has changed the 0 to a 1
--
-- As a reminder this is the definition of Run
-- Run : ( n : Nat ) -> ( x : ty ) -> ( rle : RunLength more ) ->
-- RunLength ( rep ( S n ) x ++ more )
--
-- n is set to 1, x is set to 1, and Empty means that more is set to []
-- Making the necessary substitutions results in:
-- RunLength ( rep ( S n ) x ++ more ) -- No substitutions yet
-- RunLength ( rep ( S 1 ) 1 ++ [] ) -- S 1 is the same thing as S (S Z)
-- RunLength ( 1 :: 1 :: [] ++ [] ) -- Substituting rep ( S 1 ) 1
-- RunLength ( 1 :: 1 :: [] ) -- ++ [] doesn't change our list at all
-- RunLength [ 1, 1 ] -- Syntax sugar for 1 :: 1 :: []
--
-- But this is a contradiction! Since we said in our type annotation that we
-- should have RunLength [ 1 ], not RunLength [ 1, 1 ]!
Here's the same idea in an alternative, but (roughly) equivalent, encoding, which hopefully lays it out more clearly.
RuntimeEncodedList : Type -> Type
RuntimeEncodedList t = List (Nat, t)
uncompress : RuntimeEncodedList t -> List t
uncompress runtimeEncodedList = case runtimeEncodedList of
[] => []
(n, elem) :: restOfList => rep (n + 1) elem ++ uncompress restOfList
compress : List t -> RuntimeEncodedList t
compress = ...
uncompressIsTheInverseOfCompress :
uncompress (compress xs) = xs
uncompressCorrectlyUncompressesEmptyLists = ...
This also nicely avoids a problem I see in a lot of dependently code where the structural representation of data structures are intertwined with the invariants they are supposed to uphold. Not only does this result in increasingly confusing code as the invariants get more sophisticated and also awkwardly privileges certain invariants over others, it makes modifying the representation in even the smallest ways a nightmarish test of resolve. This is because everywhere you want to create the data structure, you must also prove that the invariants hold. Sometimes this proof is trivial, sometimes this proof is difficult. But you must always do this, you cannot bail out with some sort of "believe me" escape hatch where you maybe use some sort of external solver to prove it instead, because you can now potentially crash or even segfault your program, even if your code would otherwise fulfill the invariant through some other reasoning the compiler cannot see, since the proof is an integral part of the runtime representation of the data structure.
This sort of proof burden means that it can be a Herculean task to swap out the underlying representation of the data structure for a more efficient one (e.g. you're going to be in for a hard time if you've written code with the `RunLength` type and all of a sudden, for speed reasons, you'd prefer an underlying representation of run length encoded types that groups all the run lengths in one array and stores all the actual values in another array). At least having zero multiplicity annotations on parts of the dependently typed data structure makes things a bit easier.
I instead advocate for a clean separation where the overwhelming majority of data types in a dependently-typed program should be non-dependently-typed and dependent types used instead merely to state properties about those data types independently.
The definition of `RuntimeLength` does not do away with the need to define `uncompress`, all it does is move it into the definition of `RuntimeLength`. In fact my version of `RuntimeEncodedList` and `uncompress` is less overall code than `RuntimeLength` and `uncompress`. Indeed the only reason the compiler can synthesize `uncompress` is because it duplicates `RuntimeLength`! So really the compiler hasn't reduced the amount of work that needs to be done. Just like I could've messed up my definition of `uncompress`, its equivalent in `RuntimeLength` could also have been written incorrectly. We haven't reduced the amount of code that needs to be checked by a human for correctness (in the absence of other invariants), only moved it from a function definition to a data type definition.
By moving it into a function, however, we can then selectively add as many additional properties as we want (such as the `uncompress(compress xs) == xs` invariant), without having to worry about privileging one over any other.
Instead of
append : Vector n a -> Vector m a -> Vector (n + m) a
append : List a -> List a -> List a
appendSumsLength : (xs : List a) -> (ys : List a) -> length (append xs ys) = length xs + length ys
To be clear though this is a minority position. Other programmers will argue that putting the size parameter in the data type itself makes a lot of proofs essentially trivial and that at least in the case of sized vectors, the issue of "privileging a single invariant" is less of an issue, because the only defining feature of a polymorphic list is its length. I personally disagree with the merits of this trade-off for most production code, but that's starting to get into the weeds.
I suppose laziness makes it somewhat more practical. The concrete type may only exist conceptually.
It's also unclear what constraint is being enforced. Proving that all run-length encodings decompress to some list doesn't seem interesting? This is just as true of your encoding. I suppose it would be more interesting if not every possible value of the compressed data structure were valid, such as if it contained a cached checksum that needed to match the data. We could show that all compress functions compute the checksum correctly.
But couldn't do that by having a single compress function and proving that it works? Why have more than one?
Also, it seems like verifying such a checksum would be weird. In the presence of data corruption, you would have a proof that that checksum matches the data, but by computing the checksum you could show that it doesn't match the data.
Apparently type-checking proofs aren't really about concretely showing that data is consistent? If you rely on the proof, you assume correct data rather than verifying it. A sufficiently smart compiler might optimize away your attempted verification?
I agree it's a bit tricky to understand (which is why I don't like that representation), but this has nothing to do with laziness (Idris is a strict language). It's a more general phenomenon that values in a type signature do not actually have to exist at runtime. It's purely a notational thing that lives in the type-checkers "brain" and has no runtime representation. At runtime, `compress` really does compress the list without keeping a copy of it anywhere. For any type `MyType someValue`, there's no a priori reason `someValue` should actually have any runtime representation. See e.g.
data MyType : Int -> Type
TheOnlyThingOfMyType : MyType 5
-- There's no way to actually access the 5 at runtime
-- It only lives in type signatures
someValue : MyType 5
someValue = TheOnlyThingOfMyType
-- This addition takes place at compile time, not runtime
someOtherValue : MyType (4 + 1)
someOtherValue = TheOnlyThingOfMyType
thisFailsToCompile : MyType (4 + 2)
thisFailsToCompile = TheOnlyThingOfMyType
In this case, you can use `RunLength`'s list parameter to state more invariants, even if the list doesn't exist at runtime.
-- If two lists compress to the same thing, then they must've been the same to begin with
compressionIsLossless : RunLength xs = RunLength ys -> xs = ys
-- Here follows the proof of that statement
-- If the proof looks confusing, https://shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html might help
compressionIsLossless runLengthsAreEqual = case runLengthsAreEqual of
Refl => Refl
> But couldn't do that by having a single compress function and proving that it works? Why have more than one?
I only have one compress function (I was just too lazy to write it out and used ellipses instead).
> Proving that all run-length encodings decompress to some list doesn't seem interesting? This is just as true of your encoding.
The constraint is fairly simple, but very strong (although I made a typo where the name associated with the type signature and the actual implementation's name are different, d'oh):
uncompressIsTheInverseOfCompress : uncompress(compress xs) = xs
uncompressIsTheInverseOfCompress = ... -- Too lazy to write out the actual proof at the moment
You could also of course add all sorts of other properties.
-- Even though it won't inflate list length, it can result in more memory usage due to the tuples
compressWontInflateSize : (length (compress xs) <= length xs) = True
compressWontInflateSize = ... -- Again too lazy to write out the proof
-- Idris doesn't have a general exists statement so we need to provide a
-- concrete example
compressMakesAtLeastOneListSmaller : (length (compress [1, 1, 1]) <= length [1, 1, 1])) = True
compressMakesAtLeastOneListSmaller = Refl
-- This proof is easy, just tell Idris to actually do the calculation (at compile-time, not run-time!)
I'm not sure what you mean here. In order to show that your data is consistent you need to describe what you mean by consistency somehow. You can do that either within the definition of a type itself (which I do not like) or you can do that by explaining how different functions are supposed to relate to each other (e.g. how compress, uncompress, and length should be related to each other), which I like more.
As for "optimizing away verification," that's the point of Idris' 0 multiplicity. It marks something as "compile-time-only" that has no runtime representation and hence no runtime performance impact.