8 ms·

Towards Idris Version 1.0

• hood_syntax 10y ago
  Great to see. Idris is pretty much the final frontier for what I see value in becoming comfortable with as far as functional programming goes. Hopefully it gets more momentum moving forward.
  • the_duke 10y ago
    The post says "Idris is still primarily a research project". So I wouldn't count on too much momentum. ;)
    • hood_syntax 10y ago
      Well, you're right. But that's where Haskell came from, so I'm not giving up hope just yet!
• gcanti 10y ago
  what's the state of the JavaScript backend? I do frontend and I'd really love to write some code in idris
  • adilparvez 10y ago
    Take a look at PureScript [1], it's Haskell-like but strict. [1]: http://www.purescript.org/ http://www.purescript.org/
• chriswarbo 10y ago
  Sounds good! I played with Idris quite a bit in the early days. I started spending more time in Coq around the time Idris gained its proof search mechanisms (I'm still not sure how they work!), but Idris has always been a more 'realistic' language for development (as opposed to proof engineering). I think I spoiled myself with dependent types, as all of my Haskell projects seem to hit a wall which dependent types can trivially solve (e.g. calculating a type or a TypeRep based on incoming JSON data)
  • hood_syntax 10y ago
    Dependent types are the big win for me as well, even though I'm pretty inexperienced with both Haskell and Idris. I've heard LiquidHaskell thrown around when people talk about dependent types, have you looked into that before?
    • chriswarbo 10y ago
      As far as I'm aware, LiquidTypes focus on very simple use cases, like length-indexed Vector types and such. I don't think it can manage "full" dependent types, for example situations I often find myself in where I want to calculate a type from incoming data, e.g. something like: parseJSON : String -> Maybe JSON parseJSON = ... parseMyData : JSON -> Maybe MyData parseMyData = ... HasSomeProperty : MyData -> Type HasSomeProperty x = case x of MyCase1 -> ... ... someProcessing : (x : MyData) -> HasSomeProperty x -> ResultOfProcessing x someProcessing x p = ... Often, we write "HasSomeProperty" such that it performs some arbitrary calculation to decide between returning the unit type ("does have this property") or returning the empty type ("doesn't have the property, or can't tell"). Whenever we need to provide a value of type "HasSomeProperty x", we just put a unit value and the type-checker will enforce that our arbitrary calculation resulted in a unit type. We can then use that property to access a bunch of functionality which the compiler would otherwise forbid us from using. This sort of code is trivial in a dynamically typed language: there's no requirement to prove anything, so we don't need any "HasSomeProperty x" values at all: we just go ahead and use whatever code we like, and hope that we didn't mess something up. We hit problems when we want to write our program in a language like Haskell with a (relatively) weak type system: the type system quite rightly forbids us from writing the unsafe version that dynamic languages would accept, but the language isn't expressive enough for us to (easily) encode the proofs required to convince the type checker that what we're doing is safe.
      • hood_syntax 10y ago
        Thanks for the writeup, broke it down nicely
      • 10y ago
• tupshin 10y ago
  Is anybody still thinking about Idris and HoTT? https://github.com/fmota/HoTT-Idris/blob/master/README.md https://github.com/fmota/HoTT-Idris/blob/master/README.md I don't see anything more recent than the 2014 discussions.
• chriswarbo 10y ago
  Any ideas why the effect system may be deprecated in favour of the state machine/indexed monads system? To me, they seem to be fulfilling two different requirements: algebraic effects let us call 'operations' in an expression by writing placeholder values, track the usage of such operations in the type, and plug in the implementation afterwards. For example, we can write "print" as a placeholder, give it a "StdOut" effect type, and provide a production implementation which writes to the program's stdout, a test implementation which produces a normal String value for us to check, a remote implementation which writes to a WebSocket, etc. The state machine stuff seems to mostly be concerned with using types to keep track of state, in terms of which actions are available or unavailable, e.g. you can't close a file unless it's open, you can't read from a file unless it's open, you can't run an expression unless it closes all of its files, etc. There's certainly overlap, but I'm not sure whether one subsumes the other.
  • bjz_ 10y ago
    Yeah, as someone who is interested in implementing an effect system in a language, I'd also love to know why the new approach is being considered.
  • pseudonom- 10y ago
    Extensible effects arise from combining a free monad with an open union of functors. Using an indexed free monad with indexed functors instead is a generalization that provides more expressive power. Intuitively, I like to think of it as: - Extensible effects describe what we permit (read from console, print to console) - Indexed monads describe what we demand (you must auth before you can access db, you must open file before you can read it) I'm actually working on doing a version of this in Haskell. You can see Oleg's version of it here: http://okmij.org/ftp/Haskell/extensible/ParamEff1.hs http://okmij.org/ftp/Haskell/extensible/ParamEff1.hs I may have a more informed opinion after I read the states-all-the-way paper.
    • bjz_ 10y ago
      Any more papers/resources I can look at to get more context on the indexed monads vs effect systems comparison? Are they as composable as effects - ie. how do they solve the problems with monad transformers, etc?
• weavie 10y ago
  This is pretty exciting. I'm still only about halfway through the book, but I am really enjoying the language. Learning it has been a real brain melter (in a good way) so far. Am looking forward to finishing the book. I do appreciate how you can use dependant types as much or as little as you like, so in some ways it can actually be considered a simpler and easier to learn Haskell due to having strict evaluation.
• amckinlay 10y ago
  Would be nice to see a dependently-typed strict functional programming language that didn't require a GC or a C runtime. Are there any plans for this with Idris?
  • thinkpad20 10y ago
    You could look at ATS. I don't know a huge amount about it but I know it's a very high-performance bare-metal language with dependent types, or at least, more expressive types than Haskell/ML. (Caveat: I've never written ATS, and although I've written in Coq and Idris, every time I look at ATS code it looks like complete gibberish).
    • chriswarbo 10y ago
      Most of the ATS examples begin with something which looks like ML, but as the types are made more and more strict they end up looking like incredibly verbose C. To make things worse, I don't think ATS has any inference either, so all of this must be written explicitly. Idris, Agda, Coq, etc. can infer types and values, if they're unambiguous. For example: Definition Prime p := forall n m, n * m = p -> n = 1 \/ m = 1. All of these variables have type nat, which Coq can infer from the use of "*" and "=".
  • david-given 10y ago
    Function programming with no garbage collector is tough. There is a formalisation for dealing with this, called linear logic, which allows you to statically determine object lifetimes; but it's, um, a bit awkward. Such as, every value must be produced once and consumed once, so if you want to look at a variable, you need to produce a new variable with the same value (which must be consumed later). The seminal linearly typed language is Linear Lisp, which is almost incomprehensible, and also a proof-of-concept which doesn't do anything useful. Classic paper here: http://home.pipeline.com/~hbaker1/LinearLisp.html http://home.pipeline.com/~hbaker1/LinearLisp.html The closest thing to a modern language that uses them exclusively (Rust doesn't, by the way) is LinearML, which was an experimental toy, now abandoned. Tutorial here, which may be interesting: https://github.com/pikatchu/LinearML/wiki/Tutorial https://github.com/pikatchu/LinearML/wiki/Tutorial I asked about it on StackOverflow a while back, and it collected a bunch of useful resources, including links to some of the seminal papers: http://stackoverflow.com/questions/5065861/programming-languages-based-on-linear-types http://stackoverflow.com/questions/5065861/programming-langu... (Still looking for a modern pure linear typed language, by the way.)
• alphanumeric0 10y ago
  I've been learning Haskell and Idris off and on now for a few years. I have a few friends who happen to be computer science majors and they tend to be very dismissive of Haskell, they mostly focus on the performance tweaking of a Haskell program, which seems to be a 'black art'. Does anyone know if Idris improves on this aspect of Haskell?
  • hood_syntax 10y ago
    Idris follows the eager evaluation model, so I would assume it's easier to reason about. I wouldn't take my word for it however
  • deleted 10y ago
    [deleted]
  • thinkpad20 10y ago
    I don't think Idris is nearly as performant as Haskell. Haskell has been around for way longer and has had piles of work done on optimizing the performance of the generated code, garbage collection, etc. Haskell can be written to be very fast, although its high-level nature and laziness can make it harder to optimize than a strict/imperative language. Idris on the other hand is still very much an experimental project more focused on practical applications of dependent type theory than things like performance. However, with enough work done on its compiler, its strictness and the abundance of type information might allow it to be eventually more performant. Though, the lack of type erasure might negatively impact performance as well depending on how types work at runtime...
  • icen 10y ago
    Idris, unlike Haskell, is strict, which has the general effect of making Idris' performance a bit more predictable, and a bit more like programming in other languages. However, GHC is a phenomenal compiler, and can outperform Idris for many things; this is natural, as it's seen a lot of interest in terms of producing performant code. There are still some gotchas in Idris code. The biggest one that I can think of is indexing some type with data that doesn't manage to get erased (the usual type erasure algorithm is pretty aggressive, but it can't remove everything). Some of the most useful types for programming (as in, proving theorems about the code) are wonderfully inefficient (as an example, the inductive definition of natural number is an empty linked list - taking up plenty of space in pointers, and killing your cache whenever it's accessed - Idris knows about Nat, but not about other types). Operations on the data, which might look very efficient, can also end up operating on the indices, which might not be. Here's the docs explaining the possible hiccup with erasure: http://docs.idris-lang.org/en/latest/reference/erasure.html http://docs.idris-lang.org/en/latest/reference/erasure.html
• posterboy 10y ago
  Quick question, does design by contract, ie. invariants and so on, warrant calling dependent typing? I'm currently learning OCL, and Haskell next, hence the question.
• vesak 10y ago
  How are packages handled in Idris? Do they have a cargo/composer/npm analogue?