Idris 2: Quantitative Type Theory in Practice

by otoburb • 4 years ago

150 60 4 years ago

I had a quick read of the paper and I think I got about 10% of the content - which is better than my usual average. My take-away - linear types allow you to express conditions such as this function must not be called with an empty list - QTT types extend linear types and allow you to specify run time dependencies between functions in the type system. I got the rough idea of being able to express a state machine in the type system - gives you the ability to say that this function can only be called in this state - to enter the state, these functions must be called in this order. How did I do ? Is that the rough gist of the paper ?

jlrubin• 4 years ago

you got it flipped. Dependendent types enable you to do things like "takes a nonempty list" and "returns a nonempty list of greater size".

Linear types lets you do things like "this data can only be written to a file once".

gavinray2• 4 years ago

Scala 3 is the only "functional" language that made me not feel like an idiot, and it's great for understanding "Dependent Types" as a layman.

It gives the example of a key in a database, which can return multiple types of values:

  type DB = (k: Key) => Option[k.Value]

Where the type of "Key" is:

  trait Key { type Value }

You can declare generic values of type "Key[Value]" and attempting to look them up in the DB can result in more than one kind of type, dependent on the value being looked up.

https://docs.scala-lang.org/scala3/book/types-dependent-func...

ozmaverick722• 4 years ago

Yip you are right I got that screwed up.

gavinray2• 4 years ago

Disclaimer: I'm not very bright, and don't write Idris

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:

https://github.com/tweag/linear-base/tree/master/examples

dwohnitmok15• 4 years ago

I've drank too much so I can't conjure many to mind

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.

paavohtl2• 4 years ago

As a practical example Rust uses a less powerful version of linear types called affine types for its ownership system. Values are moved by default in assignments and function calls, and they cannot be used (in their original location) after the move.

throwaway81523• 4 years ago

Linear logic is logic where any value must be used exactly once, i.e. if a=3 and you say b:=a, then b becomes 3 and a becomes undefined. The value is moved rather than copied. That is useful for describing e.g. resource management systems. If I transfer a resource to you, then you have it but I no longer do. Linear types basically means a type system that enforces linear logic.

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 ;).

gadmm• 4 years ago

Baker's paper is visionary in that it announces a link between linear logic and move semantics for resources more than a decade in advance. As we know this was put into practice by C++ and Rust. Compared to linear types, it amounts to operating a change of perspective from the quantitative interpretation (is it copied? is it dropped?) to a qualitative one (how is it copied? how is it dropped?). This is very much in spirit of linear logic (though it takes a bit of work to relate these ideas to Girard's mathematics). It answers questions that linear types were never able to, such as how to mix linearity and control. I take this paper as an example that there is more to linear logic than linear types!

chriswarbo• 4 years ago

linear types allow you to express conditions such as this function must not be called with an empty list

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) + ...

Where:

- `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) + ...

Just using the normal rules of arithmetic, we can see that NonEmptyList<T> is the same as List<T>, except everything has been multiplied by 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>

Hence we can implement NonEmptyList<T> as the type 'T × List<T>', i.e. tuples containing a T and a List<T>. Intuitively, those are the "head" and "tail" of the non-empty list; or equivalently, Cons constructs a tuple, and non-empty lists are those whose outermost constructor is always Cons.

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>

This time, we a value of type List<T> is either a unit value (representing the empty list), or a non-empty list. This pattern of "adding one" to a type is usually called 'Maybe' or 'Option':

    Maybe<T> = 1 + T

Hence simplifying the above to:

    List<T> = Maybe<NonEmptyList<T>>

mbrodersen5• 4 years ago

Idris is a really interesting language. One of the few languages that are really pushing the leading edge while trying to also be pragmatic.

skybrian3• 4 years ago

This sounds very neat in principle, but it doesn’t seem very easy to understand the code in practice. In particular:

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?

rq1• 4 years ago

You’re overthinking it. In Idris, types can be computed.

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]

skybrian3• 4 years ago

The definition of RunLength looks like two functions for uncompressing a list, given that you already have all the data from within the compressed list. The output of the function is a type containing the uncompressed data.

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.)

dwohnitmok15• 4 years ago

A sibling comment correctly lays out what the type means, and I'll elaborate a little more here.

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 ]!

However I agree with you that this style of dependently typed programming is confusing and ultimately in my view, a bad representation of how dependent types should be used in production code (if any full-spectrum dependently typed language gains enough adoption to be used in large production projects).

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 = ...

I hope this is a much plainer and easier to understand representation, with a similarly strong invariant. The `...` are of course eliding a lot, but my point is that they can be elided, without really affecting comprehension of the overall code (which is not the case with the other representation).

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.

throwaway17_17• 4 years ago

The line of thought you are expressing here really reminds me of the work on Zombie, a research language that Stephanie Weirich, among many others, worked on. In particular was the dissertation research by Chris Casinghino. He gave a talk at Boston Haskell [1] that has some really well argued points that argue for your perspective in many respects.

1 — https://m.youtube.com/watch?v=_2jrmgO_Gq0

atennapel2• 4 years ago

I haven't written enough dependently typed programs to know what's best, but just an argument in favour of the OP version :): I agree that your version is easier to understand. But with the other version the types at least guide you in the implementation of the compress/uncompress. In your version you can return any `List t`.

skybrian3• 4 years ago

Isn't it a bit odd that the type signature "contains" the uncompressed data? There would seem to be no point in compressing data this way.

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?

Jenz• 4 years ago

Idris is a truly delightful languge. It’s very comfortable coming from ML style languages; though i wish the stdlib was a little more complete…

valenterry• 4 years ago

Btw, this is extremely practical. For instance, you can then easily emulate other languages (such as SQL) natively with the typesystem and get all the benefits of the compiler/IDE, rather than having to use a library with custom syntax or a raw SQL string and having syntax/semantic errors very late at runtime only.

That alone is worth it imho.

lang_agnostic4• 4 years ago

Hi there,

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

dwohnitmok15• 4 years ago

I'm curious if you have any insight into what a realistic lower limit to Idris compile time speed looks like. Right now even moderately sized Idris programs can be quite slow to compile, slower than even other dependently-typed languages (see e.g. https://github.com/AndrasKovacs/smalltt). How much of this is intrinsic to Idris' language design and how much of it is due to lack of optimization in the implementation?

lang_agnostic4• 4 years ago

I reckon we can get the raw performance quite low, but it might be a challenging environment to program in, the ergonomics of programming linear types aren't figured out and it would involve a lot of memory management. While safe, reasoning about memory can be quite hard, just like anyone learning how to handle the borrow checked in rust can tell you.

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

Tainnor4• 4 years ago

I'm working through the Type-Driven Development with Idris right now and I can only recommend it (it's written by the creator of Idris).

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.

mbrodersen5• 4 years ago

Dependent Types can encode all of math (see the Lean math library for example). So there doesn’t really seem to be any limit to what you can do with Dependent Types. However it might of course be impractical to actually do it in some cases.

Tainnor4• 4 years ago

Of course, you can encode all of maths with it, but only in certain specific ways and not others.

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.

phlip9• 4 years ago

I was a bit disappointed with linearity in QTT as I couldn't figured out how to create a safe API around a resizable array.

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).

dwohnitmok15• 4 years ago

I thought I'd read over `Data.Linear.Array` before, but maybe not? My intuition for linear types would be that for any function that uses the array you basically almost always want to return a pair of the value and new linear version of the array (i.e. `Res a (const (arr t))`). The only exceptions are a set of "terminal" operations that convert it to a non-linear type (in this case probably the things that end up returning an `IArray`).

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

This is e.g. how Linear Haskell does it. The unrestricted multiplicity of the argument to `MkUnrestricted` prevents the bug here by only allowing you to output non-linear things (so it rejects wrapping the linear input in `MkUnrestricted`; you have to first convert it via a terminal operation into something else).

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.

mbrodersen5• 4 years ago

Here is an example of a tiny toy compiler proven correct in Idris. It is a small example of the kind of cool things you can do in Dependently Typed languages: https://github.com/mbrodersen/idris-sandbox/blob/master/comp...

Idris 2: Quantitative Type Theory in Practice

Related Stories