14 ms·

Things that Idris improves things over Haskell

221 points by deque-blog 9y ago

mijoharas 9y ago
Can anyone explain the last point to me? How exactly is the example considered "abuse"? What would an attempt to write similar in Haskell look like?
- icen 9y ago
  The 'abusiveness' is the use of `>>=` as a constructor, instead of its more standard role as member of an interface. The author is using it to take advantage of syntactic sugar that is now reliant only on names and types, instead of implementation of the relevant interface. A similar idea is to use `::` and `Nil` as constructors, which let you use the `[a, b, c]` list syntax (desugared to `a :: b :: c :: Nil`) for things that aren't actually lists. It can be convenient, but can also result in confusion.
alphonse23 9y ago
Was this written in a hurry? There's lot of spelling/grammar errors in the article.
hbex5 9y ago
Idris is one of those languages that when I learned it felt like it was offering me a glimpse into a possible future. I love it when that happens.
- runeks 9y ago
  Would you mind sharing what it was about Idris that made you feel like you were offered a glimpse into a possible future?
  - tybit 9y ago
    I can't speak for op but I had a similar feeling going through the free chapters of 'Type driven development with Idris'. What blew me away was once you have such a strong type system it eliminates whole classes or errors at compile time I previously considered only checkable at runtime. Furthermore it showed that doing so allows the compiler to go from being a gatekeeper to being more of a virtual assistant that helps you write your code not just check it.
    - runeks 9y ago
      > What blew me away was once you have such a strong type system it eliminates whole classes or errors at compile time I previously considered only checkable at runtime. Can Idris turn Haskell runtime errors into compile-time errors and, if so, which ones?
      - bbatha 9y ago
        The classic one is the `head` function in idris can only be called on `Vec`s of length 1 or more. More pressingly, you can actually prove lawfulness of type classes.
        aaron-santos 9y ago
        I'm curious how does this compare to something like Cats' NonEmptyList[1] in Scala? [1] - https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/data/NonEmptyList.scala https://github.com/typelevel/cats/blob/master/core/src/main/...
      - dynamic 9y ago
        Checking the head of an empty list is a simple example. (Although see https://wiki.haskell.org/Non-empty_list https://wiki.haskell.org/Non-empty_list for an approach to avoiding these runtime errors in Haskell). Here's a more advanced example: https://news.ycombinator.com/item?id=14569605 https://news.ycombinator.com/item?id=14569605.
      - pyrale 9y ago
        head [] in haskell will crash and burn, because you cannot carry vector size information in the type (at least not easily). In idris, you can lift the non-empty list check at type level, making such operation a compilation error.
rnhmjoj 9y ago
The problem with working with strings in Haskell is that there are too many datatypes: Data.Text, Data.Text.Lazy, Data.ByteString Data.ByteString.Char8, Data.ByteString.Lazy, Data.ByteString.Lazy.Char8. All of them share the same function names so you have to do imports like import qualified Data.ByteString as BS import qualified Data.Text.Lazy as TL import qualified Data.Text as TS and somehow the library you need always use a different ByteString variant from the one you already chose so you have to pack/unpack here and there. There should be a way to make `length`, `map` and all work on every string type. Maybe a type class or some better idea is needed. By the way the link to the caesar cipher is broken.
- runeks 9y ago
  I'm not familiar with UTF-8, which -- I believe -- is what Data.Text is used to represent. Do all UTF-8 strings have a well-defined length? A list of ASCI chars obviously does (the length of the list), but I'm not sure about Data.Text.Text.
  - rnhmjoj 9y ago
    Yes, I'm sure the length of a UTF-8 string is something tricky but Data.Text has a length function nonetheless. The APIs are very similar if not identical. You can see it here: https://hackage.haskell.org/package/text-1.2.2.2/docs/Data-Text.html https://hackage.haskell.org/package/text-1.2.2.2/docs/Data-T... https://hackage.haskell.org/package/bytestring-0.10.8.1/docs/Data-ByteString.html https://hackage.haskell.org/package/bytestring-0.10.8.1/docs...
    - HelloNurse 9y ago
      Of course, a real string type would store length along with the characters, making the length function trivial and fast.
      - leshow 9y ago
        It's hard to say what length should be because it could mean different things. How many u8 values there are? How many graphemes are present? If it's just counting how many u8's in a slice, that's trivial. But storing the total number of variable-length graphemes isn't. I assume that's why Data.Text's length function is O(n), and other languages that have UTF-16 or UTF-8 strings also have length functions that are linear.
pvdebbe 9y ago
I find it unfortunate how many languages treat strings as lists of chars for no clear benefit. This issue is apparent in dynamically typed languages where a function might expect either a string or a sequence, and now it all has to come down to type comparisons because both can be iterated. I think it'd be time to start treating them as atomic values instead.
- snakeanus 9y ago
  The benefit is that you reuse the build-in type for lists instead of making a new one. What benefit would not treating strings as lists of chars bring?
  - panic 9y ago
    Memory use: Unicode scalar values go up to 0x10ffff, which on most machines means a 32-bit value for each character. A UTF-8 representation can be less than 30% the size. And that's not even counting the fact that many languages (Haskell included) represent lists as a linked data structure, with the overhead of a pointer per list entry. Correctness: you often don't want to operate on individual Unicode scalar values. Extended grapheme clusters can combine multiple scalar values to form a single human-readable character, and that's usually the unit you care about. Representing a string directly as a list of extended grapheme clusters would use even more memory. Fundamentally, a string has more structure than a list representation gives you (encoded bytes vs. scalar values vs. grapheme clusters). I think it's better to expose this structure than it is to pretend a string is just a list of characters.
    - paulddraper 9y ago
      On the contrary, UTF-8 is the one that is long, up to 50% longer than UTF-32. (Unless you happen to have a disproportionate number of low code points.) No free lunches!
      - panic 9y ago
        Sure, UTF-8 isn't always the shortest, but for many common strings (like JSON-encoded objects with ASCII keys) it is much shorter than UTF-32. The point is that using a list representation means you can't do any better than UTF-32, even if you wanted to.
MichaelBurge 9y ago
Many of these you can work around with language extensions or a custom Prelude, but then you need to have been bitten by them to know that you need to work around them. I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in? Haskell is good for compilers and parsers. What's a good excuse to try Idris?
- neel_k 9y ago
  > I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in? It's a full-strength dependent type theory, but is intended primarily for use as a programming language. So the design focus is on using full dependent types to make ordinary programming easier. > What's a good excuse to try Idris? The best excuse of all: it is super fun.
- pjmlp 9y ago
  > Haskell is good for compilers and parsers. While true, the same applies to any other language in the ML family.
- johncolanduoni 9y ago
  Dependent types can help a lot when writing both of those actually. Idris' documentation contains an example interpreter that uses dependent typing (outside of theorem proving) heavily[1]. Compilers are a place where formal verification is likely worth it in some parts, particularly when writing optimization passes. I think one of the biggest advantages of dependent typing is that it lets you implement a lot of things that other languages need to add as ad-hoc language features. A good example (if you're familiar with Haskell) is typeclasses. These can be done entirely at the value level in Idris, and IIRC interfaces are just syntactic sugar over this implementation. Other examples are generics that depend on values instead of types (without resorting to tedious things like type-level integers) and cleaner replacements for a lot of macro functionality. [1]: http://docs.idris-lang.org/en/latest/tutorial/interp.html http://docs.idris-lang.org/en/latest/tutorial/interp.html
- HelloNurse 9y ago
atc 9y ago
Titlegore.
danidiaz 9y ago
An interview with the creator of Idris in the Code Podcast: https://soundcloud.com/podcastcode/edwin-brady-on-dependent-types-and-idris https://soundcloud.com/podcastcode/edwin-brady-on-dependent-... Another cool feature of Idris is elaborator reflection https://www.youtube.com/watch?v=pqFgYCdiYz4 https://www.youtube.com/watch?v=pqFgYCdiYz4 which I believe has no direct Haskell analogue (template Haskell perhaps?)
- tcopeland 9y ago
  More generally if you like functional programming, the archives of the "Functional Geekery" podcast are a great resource: https://www.functionalgeekery.com/ https://www.functionalgeekery.com/ There's at least one episode that's devoted to Idris: https://www.functionalgeekery.com/episode-54-edwin-brady/ https://www.functionalgeekery.com/episode-54-edwin-brady/
coldtea 9y ago
Wait, Idris sounds like a much improved Haskell. Any downsides (in the core language) besides the smaller community? Any chances for Haskell to get some of the same things?
- setra 9y ago
  The core is based on a different type theory. It is very unlikely that the part of GHC called "Haskell core" will make such a massive change. In general the Idris type inference is not nearly as good as Haskells. I don't mean this in the "dependent type inference is undecidable" sense, but instead just generally. Idris is also strict instead of lazy like Haskell. This is good or bad depending on who you ask. Very unlikely for it to change in Haskell though. Many of the other issues are the issues with every small language. Community size and libraries.
  - vosper 9y ago
    > In general the Idris type inference is not nearly as good as Haskells. I don't mean this in the "dependent type inference is undecidable" sense, but instead just generally. Do you know if this is just because Idris is a much less mature language than Haskell, or its it something fundamental about the design?
    - Buttons840 9y ago
      Probably both. Dependant type systems are still an area of active research.
unwind 9y ago
Admins; please consider editing the title, it has a redundant "things" that makes it hard to read and confusing. The blog post's real title ("10 things Idris improved over Haskell") is better; unless that's a problem due to being a list (which are often spammy). Seems fine/serious to me, though.
- behnamoh 9y ago
  As for the title problem, at first I was wondering whether that was a rare grammar usage that I didn't know about! But then I realized others have mentioned it, too. Admins have proven to be fast on these things... IDK why they don't correct it. Last time I wrote a comment that people didn't like, I got banned. Still, after nearly 3 months, I have only limited access to ycombinator. But this the admins don't see...
deleted 9y ago
[deleted]
Kiro 9y ago
What is the problem with strings being lists in Haskell?
- mmalone 9y ago
  There's a problem with strings being lists in general because it forces a representation that's not perfect for every use case. Keeping strings abstract and giving them their own interface (even if it's very similar to list's) lets you optimize the representation, or even specialize the representation for different use cases. You can intern, use vectors, use ropes, use tries, or any number of other crazy things. It also lets you expand the string interface beyond the list interface. Practically, certain operations end up being slow when you use the standard "strings are lists" mechanism provided by Haskell's standard library. Stuff like building a list is hard or slow for stupid reasons: Haskell uses cons lists with fast append-to-head and slow concatenation, so the common case of building a list by appending characters to the end is slow. Or you have to prepend and reverse. Stuff like that. It's dumb, but it matters. The Haskell community has reacted by creating other ways to represent strings, like `Data.Text` and `ByteString`. These representations have certain benefits, so they're widely used. This adds _another_ problem: different libraries use different representations, so you end up having to convert back and forth between them all the time. Again, this is annoying and inefficient. So yea. I think the lesson for language designers is clear. Strings are a distinct concept. Yes, they do list-like things, but they're not lists.
zimbatm 9y ago
I am not a fan of `cast` (also seen in other languages as well) as it leads to reductionist thinking. There are usually more than one way to convert from one type to another. How is Float to Int rounded? Shouldn't String to Int return conversion errors? Just looking at `cast` means I have to learn what the language decided to default to.
- houli 9y ago
  You should be able to write your own named implementation of Cast and explicitly use it when calling cast to have different casts with different semantics http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#named-implementations http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm.... But yeah, you'd still have to see what the standard library implementation does
- vosper 9y ago
  String to int returning 0 for an uncastable string seems like a terrible design. It should blow up. How otherwise can you tell between "0" and "ABC"?
  - SEMW 9y ago
    I haven't yet tried Idris (or even Haskell), so I could be misunderstanding, but surely in a pure language, a function with a type of String -> Int can't 'blow up', it can only output an Int? So if you want to tell the difference, you'd use something that outputs a (Maybe Int) rather than an Int, which'd be a wrapper around `cast` that does validation you want Looking at the interfaces tutorial[0], it gives an example of something similar: readNumber : IO (Maybe Nat) readNumber = do input <- getLine if all isDigit (unpack input) then pure (Just (cast input)) else pure Nothing [0] http://docs.idris-lang.org/en/latest/tutorial/interfaces.html http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm...
    - mbrock 9y ago
      In Haskell, such a function can definitely blow up. > :t read read :: Read a => String -> a > read "10" :: Int 10 > read "x" :: Int *** Exception: Prelude.read: no parse Haskell functions are pure, but not necessarily total.
alkonaut 9y ago
I know idris (apart from improving some haskell warts) also adds dependent types. Are there any good simple examples of dependent type use, that isnot vectors-of-length-N?
- mej10 9y ago
  The type safe printf implementation is pretty cool as another small example. https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr
- nv-vn 9y ago
  Yes. They're amazing for theorem proving (see Agda, Idris). They're also useful for refinement types, proving type class laws like for monads, etc.
  - alkonaut 9y ago
    Is there a hello world-y example of refinement types, similar to Vectors with length?
logophobia 9y ago
So, the unpack/pack solution seems a bit weird to me. Why do you need to convert a string to a list just to iterate? I'm assuming "List" is a linked list. Why not have an Iterable/Enumerable typeclass/trait/interface which is implemented by each dataset that is listly? Seems a lot more efficient and easier to understand then having to convert between representations just to iterate or change elements.
mej10 9y ago
Idris points the way to the future of programming. A few examples that I find very intriguing: 1. type safe printf: https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr 2. compile-time evidence that a runtime check will be performed: https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/So.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/bas... 3. Most of all, compile-time checking of state machine properties http://docs.idris-lang.org/en/latest/st/introduction.html http://docs.idris-lang.org/en/latest/st/introduction.html Think about being able to specify protocols in the type system and ensuring that your client and server meet the specifications. The example in that link is about user authentication. Imagine having a proof that the program can only get into a "LoggedIn" state by going through the authentication protocol.
- lodi 9y ago
  If anyone is having trouble understanding the raw code linked above, the official book[1] introduces all three of those concepts gently and intuitively. I highly recommend it! [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...
  - Buttons840 9y ago
    The book is written by the creator of the Idris language. I highly recommend it to those interested in type level programming as well.
- jlturner 9y ago
  Most functional languages have a type safe printf / sprintf (i.e. OCaml, F#, Haskell) which is similar to the effect you get in Idris: the types required to apply the function are statically analyzed from the format string. Edit (links): OCaml: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.html https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.ht... F#: https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual/core.printf-module-%5Bfsharp%5D https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual... Haskell: https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-Printf.html https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-P...
insulanian 9y ago
How does Idris compare to Agda (1) and F* (2)? [1] http://wiki.portal.chalmers.se/agda http://wiki.portal.chalmers.se/agda [2] https://fstar-lang.org/ https://fstar-lang.org/
- haskellandchill 9y ago
  From using Agda it is fairly similar since both do theorem proving by programming in a unified language vs Coq which has separate languages for programming and proving. Where Idris excels is a standard library focused on systems programming, things like good console input/output support that Agda doesn't focus on.
- nv-vn 9y ago
  Agda is primarily a theorem prover, Idris doesn't try to compete with that. They're rather similar in a lot of ways, but Idris targets more general purpose programming. F* is more similar in its goals, but it kind of has its own paradigm. I think a lot of the focus behind F* was based on crypto applications, so it's a bit less general purpose. It also approaches I/O without monads (to my understanding, it just uses Tot, ML, etc. to mark effects for types). The syntax is more ML-like (not super important), but in terms of the type system it's very strange compared to Idris (it focuses on refinement types versus using things like GADTs to construct a lot of the primitives -- the F* way of creating nat is to assert that an integer is >= 0 instead of defining the natural number as Zero | Succ Nat).
  - weavie 9y ago
    Indeed. Idris aims to be "PacMan complete". As in it should be perfectly feasible to write PacMan using Idris.
- platz 9y ago
  Idris & Agda are based on calculus of constructions F* is based on type refinements and smt solver. in theory all DT are equivalent but type refinements are less expressive in practice than CoC. sometimes the smt solver gives up and you are in trouble. alternatively the smt solver can provide simple refinements with less effort than CoC when it does work.
nv-vn 9y ago
Idris is a really great language and I recommend that anyone struggling with Haskell give it a try. As an OCaml programmer struggling to adjust to Haskellisms, I (ironically) ended up learning Idris before Haskell. Some of the features -- strict evaluation by default, IO evaluation vs. execution, more alternatives to do notation, better records, effects instead of monad transformers -- make Idris vastly easier to understand as a beginner despite the use of dependent types. As a language, Idris is still lacking a couple of things I'd like (and there's still plenty of bugs), but it definitely feels like it's a much refined version of Haskell.
harveywi 9y ago
Frustrated Scala users take note: Idris can compile to JVM bytecode (https://github.com/mmhelloworld/idris-jvm https://github.com/mmhelloworld/idris-jvm), JavaScript (displacing Scala.js), and native code (displacing Scala Native). Idris may be a very good choice for a post-Scala language. One thing that I find strange, though, is that some of the most prolific Scala developers who are critical of the language seem to stick to languages such as Haskell/Eta and PureScript. Maybe it's the immaturity of the Idris ecosystem.
- zzalpha 9y ago
  How does Idris' Java compatibility compare? Simply compiling to the JVM is nice, but unless it can cleanly interoperate with the rest of the Java ecosystem, it simply cannot take the place of something like Scala.
  - mbizzle88 9y ago
    I recently experimented with the Idris JavaScript backend and it is not ready for prime-time. In particular, the FFI doesn't handle functions well. I was unable to call into Idris code from JavaScript which is a deal-breaker, IMO.
- virtualwhys 9y ago
  What about non-frustrated Scala users, should they drop Scala and Scala.js in favor of an effectively experimental language with zero industry adoption? Post-Scala is already under way with the new compiler, Dotty[1], which will replace present day Scala. [1] https://github.com/lampepfl/dotty https://github.com/lampepfl/dotty
  - paulddraper 9y ago
    Non-frustrated Scala user here. I recommend you not switch in that case. You'll have to admit though: the greatest strength and weakness of Scala is Java.
hota_mazi 9y ago
Wow, I didn't realize that record field names have to be unique in Haskell. The following: data Human = Human {name :: String} data Dog = Dog {name :: String} is illegal, because they can't both have a field accessor called `name`. That's... crazy.
- steven777400 9y ago
  They only have to be unique per module. As of GHC 8.0, there is a flag that enables duplicate record names.
- mmalone 9y ago
  Yea... in theory it makes sense. In Haskell, field names are functions. If you have an instance of Human and you want it's name you do 'name human' not 'human.name()'. Polymorphism is done through type classes, not by ad-hoc overloading. So if you want the name function to take a Human or a Dog you need to define a type class with name and have both implement it (kind of like interfaces, but not really). Pragmatically, it's really annoying. There's a solution in the space between pure (a la Haskell) and magical (a la Scala) that makes sense. I think Idris might have found it.
  - mrkgnao 9y ago
    AFAIK -XDuplicateRecordFields and -XOverloadedRecordFields solve this now, creating a typeclass for each of the record labels. In this case, the compiler would generate a HasName class. (This is conceptually similar to classy lenses, but minus the TH.)
gjem97 9y ago
Presumably one of the applications of a compiler with a built-in theorem prover is mission critical code. But my understanding is that most mission critical code environments prohibit recursion. What's the main target usage here?
- mmalone 9y ago
  I've never worked on something "mission critical," but most common uses of recursion are tractable, so I'm not sure why it would be disallowed. The simplest form of tractable recursion is where some argument in the recursive call is, by some metric, "smaller" than the outer call, and is heading towards a base case that terminates recursion when the argument reaches "zero." Two examples are: decrementing integers towards zero, and recursing on the tail of a list. You can prove termination and many other properties of such a function by induction. This concept is fairly easy to generalize to any algebraic data type, and to many other domains. Edit: I realized I didn't really answer your question. The folks who are working on dependently typed languages (like Idris) see them as broadly useful, and they have a good point. Consider Java generics: they let you have types that depend on other types, like a "List of Integers." The compiler can make guarantees based on that type information and a lot of people consider that useful. With dependent types you can have types that depend on _values_, like "List of exactly 5 Integers that are all between 0 and 100." Again, the compiler can make guarantees based on that type information, and it could improve code safety, modularity, etc. The challenge with dependently typed languages has been coming up with a "surface syntax" that's easy to use. Idris (and Agda) are pretty much state of the art there.
  - regularfry 9y ago
    "most common uses are tractable" does not guarantee that many common uses will have been correctly analysed. As to why it's disallowed: stack space is limited, and tail call optimisation isn't taken for granted. Here's what the Joint Strike Fighter coding standards (thataway -> http://www.stroustrup.com/JSF-AV-rules.pdf http://www.stroustrup.com/JSF-AV-rules.pdf) say: AV Rule 119 (MISRA Rule 70) Functions shall not call themselves, either directly or indirectly (i.e. recursion shall not be allowed). Rationale: Since stack space is not unlimited, stack overflows are possible. Exception: Recursion will be permitted under the following circumstances: 1. development of SEAL 3 or general purpose software, or 2. it can be proven that adequate resources exist to support the maximum level of recursion possible. So yes, you're allowed it if you do that extra work, but given that you can replace tractable recursion with a loop anyway, the win you'd have to get from expressing the problem recursively has to compensate.
penpapersw 9y ago
Idris style/semantics question: why does the last line of the first example in the article use parentheses[1] instead of another dollar sign[2]? [1] caesar_cipher : Int -> String -> String caesar_cipher shift input = let cipher = chr . (+ shift) . ord in pack $ map cipher (unpack input) [2] caesar_cipher : Int -> String -> String caesar_cipher shift input = let cipher = chr . (+ shift) . ord in pack $ map cipher $ unpack input To me the second one seems more readable. Are there semantic differences? Performance differences?
iso-8859-1 9y ago
Interfaces are as powerful as modules in ML: 'Interfaces in Idris are similar to Haskell type classes, but with support for named overlapping instances. This means that we can give multiple different interpretations to an interface in different implementations, and in this sense they are similar in power to ML modules (Dreyer 2005). Interfaces in Idris are 1st class, meaning that implementations can be calculated by a function, and thus provide the same power as 1st-class modules in 1ML (Rossberg 2015).' Quoting from https://www.idris-lang.org/drafts/sms.pdf https://www.idris-lang.org/drafts/sms.pdf

221 points by deque-blog 9y ago

Can anyone explain the last point to me? How exactly is the example considered "abuse"? What would an attempt to write similar in Haskell look like?

icen 9y ago
The 'abusiveness' is the use of `>>=` as a constructor, instead of its more standard role as member of an interface. The author is using it to take advantage of syntactic sugar that is now reliant only on names and types, instead of implementation of the relevant interface. A similar idea is to use `::` and `Nil` as constructors, which let you use the `[a, b, c]` list syntax (desugared to `a :: b :: c :: Nil`) for things that aren't actually lists. It can be convenient, but can also result in confusion.

alphonse23 9y ago

Was this written in a hurry? There's lot of spelling/grammar errors in the article.

hbex5 9y ago

Idris is one of those languages that when I learned it felt like it was offering me a glimpse into a possible future. I love it when that happens.

runeks 9y ago
Would you mind sharing what it was about Idris that made you feel like you were offered a glimpse into a possible future?
- tybit 9y ago
  I can't speak for op but I had a similar feeling going through the free chapters of 'Type driven development with Idris'. What blew me away was once you have such a strong type system it eliminates whole classes or errors at compile time I previously considered only checkable at runtime. Furthermore it showed that doing so allows the compiler to go from being a gatekeeper to being more of a virtual assistant that helps you write your code not just check it.
  - runeks 9y ago
    > What blew me away was once you have such a strong type system it eliminates whole classes or errors at compile time I previously considered only checkable at runtime. Can Idris turn Haskell runtime errors into compile-time errors and, if so, which ones?
    - bbatha 9y ago
      The classic one is the `head` function in idris can only be called on `Vec`s of length 1 or more. More pressingly, you can actually prove lawfulness of type classes.
      - aaron-santos 9y ago
        I'm curious how does this compare to something like Cats' NonEmptyList[1] in Scala? [1] - https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/data/NonEmptyList.scala https://github.com/typelevel/cats/blob/master/core/src/main/...
    - dynamic 9y ago
      Checking the head of an empty list is a simple example. (Although see https://wiki.haskell.org/Non-empty_list https://wiki.haskell.org/Non-empty_list for an approach to avoiding these runtime errors in Haskell). Here's a more advanced example: https://news.ycombinator.com/item?id=14569605 https://news.ycombinator.com/item?id=14569605.
    - pyrale 9y ago
      head [] in haskell will crash and burn, because you cannot carry vector size information in the type (at least not easily). In idris, you can lift the non-empty list check at type level, making such operation a compilation error.

rnhmjoj 9y ago

The problem with working with strings in Haskell is that there are too many datatypes: Data.Text, Data.Text.Lazy, Data.ByteString Data.ByteString.Char8, Data.ByteString.Lazy, Data.ByteString.Lazy.Char8. All of them share the same function names so you have to do imports like import qualified Data.ByteString as BS import qualified Data.Text.Lazy as TL import qualified Data.Text as TS and somehow the library you need always use a different ByteString variant from the one you already chose so you have to pack/unpack here and there. There should be a way to make `length`, `map` and all work on every string type. Maybe a type class or some better idea is needed. By the way the link to the caesar cipher is broken.

runeks 9y ago
I'm not familiar with UTF-8, which -- I believe -- is what Data.Text is used to represent. Do all UTF-8 strings have a well-defined length? A list of ASCI chars obviously does (the length of the list), but I'm not sure about Data.Text.Text.
- rnhmjoj 9y ago
  Yes, I'm sure the length of a UTF-8 string is something tricky but Data.Text has a length function nonetheless. The APIs are very similar if not identical. You can see it here: https://hackage.haskell.org/package/text-1.2.2.2/docs/Data-Text.html https://hackage.haskell.org/package/text-1.2.2.2/docs/Data-T... https://hackage.haskell.org/package/bytestring-0.10.8.1/docs/Data-ByteString.html https://hackage.haskell.org/package/bytestring-0.10.8.1/docs...
  - HelloNurse 9y ago
    Of course, a real string type would store length along with the characters, making the length function trivial and fast.
    - leshow 9y ago
      It's hard to say what length should be because it could mean different things. How many u8 values there are? How many graphemes are present? If it's just counting how many u8's in a slice, that's trivial. But storing the total number of variable-length graphemes isn't. I assume that's why Data.Text's length function is O(n), and other languages that have UTF-16 or UTF-8 strings also have length functions that are linear.

pvdebbe 9y ago

I find it unfortunate how many languages treat strings as lists of chars for no clear benefit. This issue is apparent in dynamically typed languages where a function might expect either a string or a sequence, and now it all has to come down to type comparisons because both can be iterated. I think it'd be time to start treating them as atomic values instead.

snakeanus 9y ago
The benefit is that you reuse the build-in type for lists instead of making a new one. What benefit would not treating strings as lists of chars bring?
- panic 9y ago
  Memory use: Unicode scalar values go up to 0x10ffff, which on most machines means a 32-bit value for each character. A UTF-8 representation can be less than 30% the size. And that's not even counting the fact that many languages (Haskell included) represent lists as a linked data structure, with the overhead of a pointer per list entry. Correctness: you often don't want to operate on individual Unicode scalar values. Extended grapheme clusters can combine multiple scalar values to form a single human-readable character, and that's usually the unit you care about. Representing a string directly as a list of extended grapheme clusters would use even more memory. Fundamentally, a string has more structure than a list representation gives you (encoded bytes vs. scalar values vs. grapheme clusters). I think it's better to expose this structure than it is to pretend a string is just a list of characters.
  - paulddraper 9y ago
    On the contrary, UTF-8 is the one that is long, up to 50% longer than UTF-32. (Unless you happen to have a disproportionate number of low code points.) No free lunches!
    - panic 9y ago
      Sure, UTF-8 isn't always the shortest, but for many common strings (like JSON-encoded objects with ASCII keys) it is much shorter than UTF-32. The point is that using a list representation means you can't do any better than UTF-32, even if you wanted to.

MichaelBurge 9y ago

Many of these you can work around with language extensions or a custom Prelude, but then you need to have been bitten by them to know that you need to work around them. I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in? Haskell is good for compilers and parsers. What's a good excuse to try Idris?

neel_k 9y ago
> I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in? It's a full-strength dependent type theory, but is intended primarily for use as a programming language. So the design focus is on using full dependent types to make ordinary programming easier. > What's a good excuse to try Idris? The best excuse of all: it is super fun.
pjmlp 9y ago
> Haskell is good for compilers and parsers. While true, the same applies to any other language in the ML family.
johncolanduoni 9y ago
Dependent types can help a lot when writing both of those actually. Idris' documentation contains an example interpreter that uses dependent typing (outside of theorem proving) heavily[1]. Compilers are a place where formal verification is likely worth it in some parts, particularly when writing optimization passes. I think one of the biggest advantages of dependent typing is that it lets you implement a lot of things that other languages need to add as ad-hoc language features. A good example (if you're familiar with Haskell) is typeclasses. These can be done entirely at the value level in Idris, and IIRC interfaces are just syntactic sugar over this implementation. Other examples are generics that depend on values instead of types (without resorting to tedious things like type-level integers) and cleaner replacements for a lot of macro functionality. [1]: http://docs.idris-lang.org/en/latest/tutorial/interp.html http://docs.idris-lang.org/en/latest/tutorial/interp.html
HelloNurse 9y ago

atc 9y ago

Titlegore.

danidiaz 9y ago

An interview with the creator of Idris in the Code Podcast: https://soundcloud.com/podcastcode/edwin-brady-on-dependent-types-and-idris https://soundcloud.com/podcastcode/edwin-brady-on-dependent-... Another cool feature of Idris is elaborator reflection https://www.youtube.com/watch?v=pqFgYCdiYz4 https://www.youtube.com/watch?v=pqFgYCdiYz4 which I believe has no direct Haskell analogue (template Haskell perhaps?)

tcopeland 9y ago
More generally if you like functional programming, the archives of the "Functional Geekery" podcast are a great resource: https://www.functionalgeekery.com/ https://www.functionalgeekery.com/ There's at least one episode that's devoted to Idris: https://www.functionalgeekery.com/episode-54-edwin-brady/ https://www.functionalgeekery.com/episode-54-edwin-brady/

coldtea 9y ago

Wait, Idris sounds like a much improved Haskell. Any downsides (in the core language) besides the smaller community? Any chances for Haskell to get some of the same things?

setra 9y ago
The core is based on a different type theory. It is very unlikely that the part of GHC called "Haskell core" will make such a massive change. In general the Idris type inference is not nearly as good as Haskells. I don't mean this in the "dependent type inference is undecidable" sense, but instead just generally. Idris is also strict instead of lazy like Haskell. This is good or bad depending on who you ask. Very unlikely for it to change in Haskell though. Many of the other issues are the issues with every small language. Community size and libraries.
- vosper 9y ago
  > In general the Idris type inference is not nearly as good as Haskells. I don't mean this in the "dependent type inference is undecidable" sense, but instead just generally. Do you know if this is just because Idris is a much less mature language than Haskell, or its it something fundamental about the design?
  - Buttons840 9y ago
    Probably both. Dependant type systems are still an area of active research.

unwind 9y ago

Admins; please consider editing the title, it has a redundant "things" that makes it hard to read and confusing. The blog post's real title ("10 things Idris improved over Haskell") is better; unless that's a problem due to being a list (which are often spammy). Seems fine/serious to me, though.

behnamoh 9y ago
As for the title problem, at first I was wondering whether that was a rare grammar usage that I didn't know about! But then I realized others have mentioned it, too. Admins have proven to be fast on these things... IDK why they don't correct it. Last time I wrote a comment that people didn't like, I got banned. Still, after nearly 3 months, I have only limited access to ycombinator. But this the admins don't see...

deleted 9y ago

[deleted]

Kiro 9y ago

What is the problem with strings being lists in Haskell?

mmalone 9y ago
There's a problem with strings being lists in general because it forces a representation that's not perfect for every use case. Keeping strings abstract and giving them their own interface (even if it's very similar to list's) lets you optimize the representation, or even specialize the representation for different use cases. You can intern, use vectors, use ropes, use tries, or any number of other crazy things. It also lets you expand the string interface beyond the list interface. Practically, certain operations end up being slow when you use the standard "strings are lists" mechanism provided by Haskell's standard library. Stuff like building a list is hard or slow for stupid reasons: Haskell uses cons lists with fast append-to-head and slow concatenation, so the common case of building a list by appending characters to the end is slow. Or you have to prepend and reverse. Stuff like that. It's dumb, but it matters. The Haskell community has reacted by creating other ways to represent strings, like `Data.Text` and `ByteString`. These representations have certain benefits, so they're widely used. This adds _another_ problem: different libraries use different representations, so you end up having to convert back and forth between them all the time. Again, this is annoying and inefficient. So yea. I think the lesson for language designers is clear. Strings are a distinct concept. Yes, they do list-like things, but they're not lists.

zimbatm 9y ago

I am not a fan of `cast` (also seen in other languages as well) as it leads to reductionist thinking. There are usually more than one way to convert from one type to another. How is Float to Int rounded? Shouldn't String to Int return conversion errors? Just looking at `cast` means I have to learn what the language decided to default to.

houli 9y ago
You should be able to write your own named implementation of Cast and explicitly use it when calling cast to have different casts with different semantics http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#named-implementations http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm.... But yeah, you'd still have to see what the standard library implementation does
vosper 9y ago
String to int returning 0 for an uncastable string seems like a terrible design. It should blow up. How otherwise can you tell between "0" and "ABC"?
- SEMW 9y ago
  I haven't yet tried Idris (or even Haskell), so I could be misunderstanding, but surely in a pure language, a function with a type of String -> Int can't 'blow up', it can only output an Int? So if you want to tell the difference, you'd use something that outputs a (Maybe Int) rather than an Int, which'd be a wrapper around `cast` that does validation you want Looking at the interfaces tutorial[0], it gives an example of something similar: readNumber : IO (Maybe Nat) readNumber = do input <- getLine if all isDigit (unpack input) then pure (Just (cast input)) else pure Nothing [0] http://docs.idris-lang.org/en/latest/tutorial/interfaces.html http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm...
  - mbrock 9y ago
    In Haskell, such a function can definitely blow up. > :t read read :: Read a => String -> a > read "10" :: Int 10 > read "x" :: Int *** Exception: Prelude.read: no parse Haskell functions are pure, but not necessarily total.

alkonaut 9y ago

I know idris (apart from improving some haskell warts) also adds dependent types. Are there any good simple examples of dependent type use, that isnot vectors-of-length-N?

mej10 9y ago
The type safe printf implementation is pretty cool as another small example. https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr
nv-vn 9y ago
Yes. They're amazing for theorem proving (see Agda, Idris). They're also useful for refinement types, proving type class laws like for monads, etc.
- alkonaut 9y ago
  Is there a hello world-y example of refinement types, similar to Vectors with length?

logophobia 9y ago

So, the unpack/pack solution seems a bit weird to me. Why do you need to convert a string to a list just to iterate? I'm assuming "List" is a linked list. Why not have an Iterable/Enumerable typeclass/trait/interface which is implemented by each dataset that is listly? Seems a lot more efficient and easier to understand then having to convert between representations just to iterate or change elements.

mej10 9y ago

Idris points the way to the future of programming. A few examples that I find very intriguing: 1. type safe printf: https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr 2. compile-time evidence that a runtime check will be performed: https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/So.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/bas... 3. Most of all, compile-time checking of state machine properties http://docs.idris-lang.org/en/latest/st/introduction.html http://docs.idris-lang.org/en/latest/st/introduction.html Think about being able to specify protocols in the type system and ensuring that your client and server meet the specifications. The example in that link is about user authentication. Imagine having a proof that the program can only get into a "LoggedIn" state by going through the authentication protocol.

lodi 9y ago
If anyone is having trouble understanding the raw code linked above, the official book[1] introduces all three of those concepts gently and intuitively. I highly recommend it! [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...
- Buttons840 9y ago
  The book is written by the creator of the Idris language. I highly recommend it to those interested in type level programming as well.
jlturner 9y ago
Most functional languages have a type safe printf / sprintf (i.e. OCaml, F#, Haskell) which is similar to the effect you get in Idris: the types required to apply the function are statically analyzed from the format string. Edit (links): OCaml: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.html https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.ht... F#: https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual/core.printf-module-%5Bfsharp%5D https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual... Haskell: https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-Printf.html https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-P...

insulanian 9y ago

How does Idris compare to Agda (1) and F* (2)? [1] http://wiki.portal.chalmers.se/agda http://wiki.portal.chalmers.se/agda [2] https://fstar-lang.org/ https://fstar-lang.org/

haskellandchill 9y ago
From using Agda it is fairly similar since both do theorem proving by programming in a unified language vs Coq which has separate languages for programming and proving. Where Idris excels is a standard library focused on systems programming, things like good console input/output support that Agda doesn't focus on.
nv-vn 9y ago
Agda is primarily a theorem prover, Idris doesn't try to compete with that. They're rather similar in a lot of ways, but Idris targets more general purpose programming. F* is more similar in its goals, but it kind of has its own paradigm. I think a lot of the focus behind F* was based on crypto applications, so it's a bit less general purpose. It also approaches I/O without monads (to my understanding, it just uses Tot, ML, etc. to mark effects for types). The syntax is more ML-like (not super important), but in terms of the type system it's very strange compared to Idris (it focuses on refinement types versus using things like GADTs to construct a lot of the primitives -- the F* way of creating nat is to assert that an integer is >= 0 instead of defining the natural number as Zero | Succ Nat).
- weavie 9y ago
  Indeed. Idris aims to be "PacMan complete". As in it should be perfectly feasible to write PacMan using Idris.
platz 9y ago
Idris & Agda are based on calculus of constructions F* is based on type refinements and smt solver. in theory all DT are equivalent but type refinements are less expressive in practice than CoC. sometimes the smt solver gives up and you are in trouble. alternatively the smt solver can provide simple refinements with less effort than CoC when it does work.

nv-vn 9y ago

Idris is a really great language and I recommend that anyone struggling with Haskell give it a try. As an OCaml programmer struggling to adjust to Haskellisms, I (ironically) ended up learning Idris before Haskell. Some of the features -- strict evaluation by default, IO evaluation vs. execution, more alternatives to do notation, better records, effects instead of monad transformers -- make Idris vastly easier to understand as a beginner despite the use of dependent types. As a language, Idris is still lacking a couple of things I'd like (and there's still plenty of bugs), but it definitely feels like it's a much refined version of Haskell.

harveywi 9y ago

Frustrated Scala users take note: Idris can compile to JVM bytecode (https://github.com/mmhelloworld/idris-jvm https://github.com/mmhelloworld/idris-jvm), JavaScript (displacing Scala.js), and native code (displacing Scala Native). Idris may be a very good choice for a post-Scala language. One thing that I find strange, though, is that some of the most prolific Scala developers who are critical of the language seem to stick to languages such as Haskell/Eta and PureScript. Maybe it's the immaturity of the Idris ecosystem.

zzalpha 9y ago
How does Idris' Java compatibility compare? Simply compiling to the JVM is nice, but unless it can cleanly interoperate with the rest of the Java ecosystem, it simply cannot take the place of something like Scala.
- mbizzle88 9y ago
  I recently experimented with the Idris JavaScript backend and it is not ready for prime-time. In particular, the FFI doesn't handle functions well. I was unable to call into Idris code from JavaScript which is a deal-breaker, IMO.
virtualwhys 9y ago
What about non-frustrated Scala users, should they drop Scala and Scala.js in favor of an effectively experimental language with zero industry adoption? Post-Scala is already under way with the new compiler, Dotty[1], which will replace present day Scala. [1] https://github.com/lampepfl/dotty https://github.com/lampepfl/dotty
- paulddraper 9y ago
  Non-frustrated Scala user here. I recommend you not switch in that case. You'll have to admit though: the greatest strength and weakness of Scala is Java.

hota_mazi 9y ago

Wow, I didn't realize that record field names have to be unique in Haskell. The following: data Human = Human {name :: String} data Dog = Dog {name :: String} is illegal, because they can't both have a field accessor called `name`. That's... crazy.

steven777400 9y ago
They only have to be unique per module. As of GHC 8.0, there is a flag that enables duplicate record names.
mmalone 9y ago
Yea... in theory it makes sense. In Haskell, field names are functions. If you have an instance of Human and you want it's name you do 'name human' not 'human.name()'. Polymorphism is done through type classes, not by ad-hoc overloading. So if you want the name function to take a Human or a Dog you need to define a type class with name and have both implement it (kind of like interfaces, but not really). Pragmatically, it's really annoying. There's a solution in the space between pure (a la Haskell) and magical (a la Scala) that makes sense. I think Idris might have found it.
- mrkgnao 9y ago
  AFAIK -XDuplicateRecordFields and -XOverloadedRecordFields solve this now, creating a typeclass for each of the record labels. In this case, the compiler would generate a HasName class. (This is conceptually similar to classy lenses, but minus the TH.)

gjem97 9y ago

Presumably one of the applications of a compiler with a built-in theorem prover is mission critical code. But my understanding is that most mission critical code environments prohibit recursion. What's the main target usage here?

mmalone 9y ago
I've never worked on something "mission critical," but most common uses of recursion are tractable, so I'm not sure why it would be disallowed. The simplest form of tractable recursion is where some argument in the recursive call is, by some metric, "smaller" than the outer call, and is heading towards a base case that terminates recursion when the argument reaches "zero." Two examples are: decrementing integers towards zero, and recursing on the tail of a list. You can prove termination and many other properties of such a function by induction. This concept is fairly easy to generalize to any algebraic data type, and to many other domains. Edit: I realized I didn't really answer your question. The folks who are working on dependently typed languages (like Idris) see them as broadly useful, and they have a good point. Consider Java generics: they let you have types that depend on other types, like a "List of Integers." The compiler can make guarantees based on that type information and a lot of people consider that useful. With dependent types you can have types that depend on _values_, like "List of exactly 5 Integers that are all between 0 and 100." Again, the compiler can make guarantees based on that type information, and it could improve code safety, modularity, etc. The challenge with dependently typed languages has been coming up with a "surface syntax" that's easy to use. Idris (and Agda) are pretty much state of the art there.
- regularfry 9y ago
  "most common uses are tractable" does not guarantee that many common uses will have been correctly analysed. As to why it's disallowed: stack space is limited, and tail call optimisation isn't taken for granted. Here's what the Joint Strike Fighter coding standards (thataway -> http://www.stroustrup.com/JSF-AV-rules.pdf http://www.stroustrup.com/JSF-AV-rules.pdf) say: AV Rule 119 (MISRA Rule 70) Functions shall not call themselves, either directly or indirectly (i.e. recursion shall not be allowed). Rationale: Since stack space is not unlimited, stack overflows are possible. Exception: Recursion will be permitted under the following circumstances: 1. development of SEAL 3 or general purpose software, or 2. it can be proven that adequate resources exist to support the maximum level of recursion possible. So yes, you're allowed it if you do that extra work, but given that you can replace tractable recursion with a loop anyway, the win you'd have to get from expressing the problem recursively has to compensate.

penpapersw 9y ago

Idris style/semantics question: why does the last line of the first example in the article use parentheses[1] instead of another dollar sign[2]? [1] caesar_cipher : Int -> String -> String caesar_cipher shift input = let cipher = chr . (+ shift) . ord in pack $ map cipher (unpack input) [2] caesar_cipher : Int -> String -> String caesar_cipher shift input = let cipher = chr . (+ shift) . ord in pack $ map cipher $ unpack input To me the second one seems more readable. Are there semantic differences? Performance differences?

iso-8859-1 9y ago

Interfaces are as powerful as modules in ML: 'Interfaces in Idris are similar to Haskell type classes, but with support for named overlapping instances. This means that we can give multiple different interpretations to an interface in different implementations, and in this sense they are similar in power to ML modules (Dreyer 2005). Interfaces in Idris are 1st class, meaning that implementations can be calculated by a function, and thus provide the same power as 1st-class modules in 1ML (Rossberg 2015).' Quoting from https://www.idris-lang.org/drafts/sms.pdf https://www.idris-lang.org/drafts/sms.pdf