17 ms·

Idris 2: Quantitative Type Theory in Practice

150 points by otoburb 5y ago

ozmaverick72 5y 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 5y 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".
  - gavinray 5y 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-function.html https://docs.scala-lang.org/scala3/book/types-dependent-func...
    - jhhh 5y ago
      How is this different from what you can do in Java? interface Key<V> { ... } class Name extends Key<String> { ... } class Age extends Key<Integer> { ... } interface DB { public <V> Optional<V> get(Key<V> k) { ... } }
      - drdeca 5y ago
        in their example, iiuc, DB takes as input the value k, and returns a value of type Optional[k.Value] . The return type depends on the input.
        jhhh 5y ago
        I could be missing something but my example does as well since it's a method level generic: Name nameKey = ...; Age ageKey = ...; Optional<String> name = db.get(nameKey); Optional<Integer> age = db.get(ageKey);
        Mehdi2277 5y ago
        The difference is your keys are types. Dependent types are about generics where the keys are allowed to be values. You can not in Java directly do, 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.
      - lmm 5y ago
        In that Java version someone can call get<String>(age) or get<Integer>(name). In the Scala version the value type is a member of the key.
        jhhh 5y ago
        You get a compilation error if you try that.
        dwohnitmok 5y ago
        Yeah the `Key` and `DB` example, while somewhat differing in semantics, can be emulated by Java. 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)
    - DylanSp 5y ago
      I wouldn't call those dependent types, exactly, because it's still happening entirely at the type level. The defining characteristic of dependent type systems is that they allow mixing of type-level and value-level expressions. To use the classic example of appending one vector to another, Idris lets us express the type: app : Vect n a -> Vect m a -> Vect (n + m) a where we're using the value-level addition operator to express the type of the result; specifically, that appending a Vect of length m to a Vect of length n will give a Vect of length (n + m). [1] [1] Taken from https://www.idris-lang.org/pages/example.html https://www.idris-lang.org/pages/example.html
      - dwohnitmok 5y ago
        They are dependent types since they do depend on runtime values (notice in `DB` the `k` is a runtime value), rather than just types. They are, however, very restricted compared to more "full-spectrum" dependently typed languages.
    - exdsq 5y ago
      A really nice thing in Haskell beyond dependent types is refinement types. Not sure if they exist in Scala - I'm sure someone has hacked something together somewhere. https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
    - dwohnitmok 5y ago
      If Scala syntax is more up your alley, here's an intro to dependent types that has more Scala-esque syntax: https://shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html https://shuangrimu.com/posts/language-agnostic-intro-to-depe... 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).
  - ozmaverick72 5y ago
    Yip you are right I got that screwed up.
- gavinray 5y 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 https://github.com/tweag/linear-base/tree/master/examples
  - dwohnitmok 5y 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.
  - paavohtl 5y 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.
    - iopq 5y ago
      Rust already has the ability to make you use the type at most once, so the useful extension for Rust would be "must-use types" which is an extension of linear types (since linear types would be able to represented in this system easily enough) 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
- throwaway81523 5y 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-ForthStack.pdf https://hashingit.com/elements/research-resources/1994-03-Fo... Yes it's about how Forth implements linear logic without realizing it ;).
  - gadmm 5y 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 5y 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>>
mbrodersen 5y 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.
skybrian 5y 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 5y 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]
  - skybrian 5y 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.)
    - 4ad 5y ago
      > 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 That's exactly how you write GADTs in Haskell: https://downloads.haskell.org/~ghc/6.6/docs/html/users_guide/gadt.html https://downloads.haskell.org/~ghc/6.6/docs/html/users_guide....
deleted 5y ago
[deleted]
Jenz 5y 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 5y 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.
deleted 5y ago
[deleted]
lang_agnostic 5y 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 https://github.com/idris-lang/Idris2 - we have some very interesting libraries in the works: https://github.com/idris-lang/Idris2/wiki/Libraries 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 https://gitlab.com/avidela/recombine
- dwohnitmok 5y 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 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_agnostic 5y 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
Tainnor 5y 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.
- mbrodersen 5y 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.
  - Tainnor 5y 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.
    - mbrodersen 5y ago
      > but only in certain specific ways and not others. 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.
phlip9 5y 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/Data/Linear/Array.idr 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 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).
- dwohnitmok 5y 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.
mbrodersen 5y 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/compile-to-stack-machine.idr https://github.com/mbrodersen/idris-sandbox/blob/master/comp...

150 points by otoburb 5y 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 5y 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".
- gavinray 5y 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-function.html https://docs.scala-lang.org/scala3/book/types-dependent-func...
  - jhhh 5y ago
    How is this different from what you can do in Java? interface Key<V> { ... } class Name extends Key<String> { ... } class Age extends Key<Integer> { ... } interface DB { public <V> Optional<V> get(Key<V> k) { ... } }
    - drdeca 5y ago
      in their example, iiuc, DB takes as input the value k, and returns a value of type Optional[k.Value] . The return type depends on the input.
      - jhhh 5y ago
        I could be missing something but my example does as well since it's a method level generic: Name nameKey = ...; Age ageKey = ...; Optional<String> name = db.get(nameKey); Optional<Integer> age = db.get(ageKey);
        Mehdi2277 5y ago
        The difference is your keys are types. Dependent types are about generics where the keys are allowed to be values. You can not in Java directly do, 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.
    - lmm 5y ago
      In that Java version someone can call get<String>(age) or get<Integer>(name). In the Scala version the value type is a member of the key.
      - jhhh 5y ago
        You get a compilation error if you try that.
        dwohnitmok 5y ago
        Yeah the `Key` and `DB` example, while somewhat differing in semantics, can be emulated by Java. 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)
  - DylanSp 5y ago
    I wouldn't call those dependent types, exactly, because it's still happening entirely at the type level. The defining characteristic of dependent type systems is that they allow mixing of type-level and value-level expressions. To use the classic example of appending one vector to another, Idris lets us express the type: app : Vect n a -> Vect m a -> Vect (n + m) a where we're using the value-level addition operator to express the type of the result; specifically, that appending a Vect of length m to a Vect of length n will give a Vect of length (n + m). [1] [1] Taken from https://www.idris-lang.org/pages/example.html https://www.idris-lang.org/pages/example.html
    - dwohnitmok 5y ago
      They are dependent types since they do depend on runtime values (notice in `DB` the `k` is a runtime value), rather than just types. They are, however, very restricted compared to more "full-spectrum" dependently typed languages.
  - exdsq 5y ago
    A really nice thing in Haskell beyond dependent types is refinement types. Not sure if they exist in Scala - I'm sure someone has hacked something together somewhere. https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
  - dwohnitmok 5y ago
    If Scala syntax is more up your alley, here's an intro to dependent types that has more Scala-esque syntax: https://shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html https://shuangrimu.com/posts/language-agnostic-intro-to-depe... 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).
- ozmaverick72 5y ago
  Yip you are right I got that screwed up.
gavinray 5y 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 https://github.com/tweag/linear-base/tree/master/examples
- dwohnitmok 5y 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.
- paavohtl 5y 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.
  - iopq 5y ago
    Rust already has the ability to make you use the type at most once, so the useful extension for Rust would be "must-use types" which is an extension of linear types (since linear types would be able to represented in this system easily enough) 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
throwaway81523 5y 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-ForthStack.pdf https://hashingit.com/elements/research-resources/1994-03-Fo... Yes it's about how Forth implements linear logic without realizing it ;).
- gadmm 5y 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 5y 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>>

mbrodersen 5y 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.

skybrian 5y 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 5y 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]
- skybrian 5y 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.)
  - 4ad 5y ago
    > 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 That's exactly how you write GADTs in Haskell: https://downloads.haskell.org/~ghc/6.6/docs/html/users_guide/gadt.html https://downloads.haskell.org/~ghc/6.6/docs/html/users_guide....

deleted 5y ago

[deleted]

Jenz 5y 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 5y 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.

deleted 5y ago

[deleted]

lang_agnostic 5y 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 https://github.com/idris-lang/Idris2 - we have some very interesting libraries in the works: https://github.com/idris-lang/Idris2/wiki/Libraries 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 https://gitlab.com/avidela/recombine

dwohnitmok 5y 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 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_agnostic 5y 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

Tainnor 5y 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.

mbrodersen 5y 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.
- Tainnor 5y 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.
  - mbrodersen 5y ago
    > but only in certain specific ways and not others. 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.

phlip9 5y 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/Data/Linear/Array.idr 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 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).

dwohnitmok 5y 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.

mbrodersen 5y 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/compile-to-stack-machine.idr https://github.com/mbrodersen/idris-sandbox/blob/master/comp...