16 ms·

For anyone wondering what Idris is, it's pretty much Haskell with dependent types. That is, it's easy to encode thing like "vector of length n" in the type syst

by Y_Y 10y ago

For anyone wondering what Idris is, it's pretty much Haskell with dependent types. That is, it's easy to encode thing like "vector of length n" in the type system, so you can go from concat :: Vec -> Vec -> Vec to concat : Vec n -> Vec m -> Vec (n+m).

pdexter 10y ago
Though unlike Haskell, it is strict.
- asattarmd 10y ago
  Strict by default. You can make it lazy easily.
- clacke2 10y ago
  The next Haskell will be strict -- Simon Peyton Jones http://www.cs.nott.ac.uk/%7Egmh/appsem-slides/peytonjones.ppt http://www.cs.nott.ac.uk/%7Egmh/appsem-slides/peytonjones.pp... /via https://news.ycombinator.com/item?id=1924061 https://news.ycombinator.com/item?id=1924061
  - kobeya 10y ago
    Yes, but not because laziness was a technical failure, but for something more resembling PR reasons. Haskell's laziness by default ends up being a large stumbling block for many developers not used to thinking in that way. Although I understand why Idris is strict by default, there is a part of me that dies a little from that understanding :(
    - mafribe 10y ago
      The main problem with laziness is that, according to SPJ "[l]aziness makes it much, much harder to reason about performance, especially space."
      - willtim 10y ago
        Of course, lazy-by-default also brings many advantages: http://augustss.blogspot.co.uk/2011/05/more-points-for-lazy-evaluation-in.html http://augustss.blogspot.co.uk/2011/05/more-points-for-lazy-...
        deleted 10y ago
        [deleted]
    - solidsnack9000 10y ago
      It's not so much a PR failure, as an ergonomics issue -- making laziness the default makes it too easy for people to create performance problems for themselves. Haskell's laziness undoubtedly works and is useful; you might say it was Haskell's strictness that needed improving.
- pjmlp 10y ago
  Haskell is just lazy by default, you can make code explicitly strict. Just like other languages are strict by default, but can be made lazy via sequences, streams, generators,... It is just a matter which defaults might be better for a given application.
  - vram22 10y ago
    What does strict mean in this context? I don't know too much about these concepts. I think lazy means only evaluated when needed, like in generators (using Python as an example, which I know - I don't know Haskell or Idris). And I thought (from what little I've read), that the opposite of lazy evaluation was eager evaluation. So in Python at least, an example of eager vs. lazy would be returning a list vs. returning a generator from a function. For the former (list), the whole list would have to be created/populated and then returned (thereby occupying memory for the duration of its use), whereas for the latter (generator), items from it would only be yielded on demand, e.g. one at a time, when next() is called, or when the generator is iterated over, and so would not use as much memory as needed for the sum of the sizes of the items in the list. So where does strict fit in here? Feel free to point if I've got any of the above wrong. Update: Thanks for the replies, people.
    - chongli 10y ago
      Strict evaluation is a synonym for eager evaluation. In Haskell, the primary mechanism for inducing evaluation is the case expression (if/then/else and pattern matching are syntactic sugar for case). Thunks (lazy expressions) in Haskell are created with let and then forced with case. It's very straightforward at the most basic level, there's just a lot of abstraction built on top of it that can obscure what's going on.
    - laszlokorte 10y ago
      strict is same as eager and non-strict is same as lazy https://wiki.haskell.org/Lazy_vs._non-strict https://wiki.haskell.org/Lazy_vs._non-strict
    - mrkgnao 10y ago
      I wrote this a while back. You might find it of some use. https://news.ycombinator.com/item?id=13907573 https://news.ycombinator.com/item?id=13907573
CJefferson 10y ago
Yes, but it turns out you can do some cool things with dependent types. I always felt, as a C++ programmer, that Haskell was just restricting me, without providing me any real benefits (of course, other people's opinion can vary!) -- on the other hand, Idris provides tools I can see as useful, things like checking at compile time all file handles are correctly opened before use, and closed after use (that's a very simple example, but just one type of thing you can do)
- pdexter 10y ago
  I'm not sure that is quite a simple example actually. Sounds kind of complex to prove that all file handles are closed after use (how soon after use?) in the general sense, especially when they're opened dynamically. Also, you can already do half of what you described in Haskell. Just require the functions that work over open files to require an Open type which the open function would return.
  - lgas 10y ago
    If you search for the "File Management" section in this doc, you can see an example of what he's talking about. https://media.readthedocs.org/pdf/idris/latest/idris.pdf https://media.readthedocs.org/pdf/idris/latest/idris.pdf
  - chriswarbo 10y ago
    > Just require the functions that work over open files to require an Open type which the open function would return. Not quite. The problem is that values can be copied (AKA used "non-linearly"), for example: open :: FilePath -> IO Open readFile :: Open -> IO String close :: Open -> IO Closed main = do -- Open a file handle o <- open "/tmp/foo" -- Close "o" c <- close o -- Try reading from "o" s <- readFile o putStr s This program will type-check, since "o" has type "Open", so it's a valid input to "close" and to "readFile". The problem is that the type system has no idea that calling (the IO action returned by) "close o" makes subsequent uses of "o" invalid, even though it still has type "Open". With linear types, we can make "Open" and "Closed" linear. It's a type error to use a linearly-typed value more than once, which rules out the above double-usage of "o :: Open". It's also a type error to create a linearly-typed value and not use it at all; we can use this when designing an API, e.g. to make a function like: withFile :: (Open -> (Closed, a)) -> IO a The only way to call this function is to provide it with a function of type `Open -> (Closed, a)`. If we've encapsulated our implementation details, then the only way to write a function which returns a `Closed` is to have it call `close :: Open -> Close`. Since values of type `Open` can't be re-used, this must either be its argument or the return value of some call, e.g. `readFile :: Open -> (Open, String)` or `writeFile :: String -> Open -> IO Open`, which in turn require an `Open` argument, and so on; forcing a chain of operations, culminating in a `close`.
muraiki 10y ago
Another way to think of it is that types are first class. Here's an example I found of returning a type, although I forget where I found it. It's a version of a sample on the Rust page, but it now handles floats if necessary: https://paste.fedoraproject.org/paste/UTrEje4Czbiq8C0u1oJOnF5M1UNdIGYhyRLivL9gydE= https://paste.fedoraproject.org/paste/UTrEje4Czbiq8C0u1oJOnF...
- deleted 10y ago
  [deleted]
jadbox 10y ago
Does Scala have this kind of dependent types? What does Idris type system provide that Scala doesn't support?
- jackmott 10y ago
  no. in idris you can declare a functions that takes integers less than five, and if you write code that can eve theoretically allow that function to get called with 5 or greater you get a compiler error. things like that
- virtualwhys 10y ago
  Scala has path dependent types. def foo(a: Bar)(b: a.Baz) = ... Idris' dependent types are more powerful, though @edwinb would probably be the one to explain the differences in detail (he gave a talk awhile back on Scala vs. Idris).
- lmm 10y ago
  Most, possibly all, of what you do in Idris can be encoded into Scala, but working with type-level functions become very cumbersome. The compiler doesn't understand that a type-level function is a function, so every time you apply a function to a type and need to know the result is the same as itself you have to summon evidence that this is so (which also sends compile times through the roof). Higher-kinded types get treated differently for equality unless you encode them as members of wrapper types. You end up having to write all your type-level stuff in a kind of continuation-passing style and defining intermediate types to represent each step of your algorithm.
kemiller2002 10y ago
There are other differences too. The syntax is very very close, but how it handles things like evaluation is different. Don't assume that just because they look the same that they are.

by Y_Y 10y ago

pdexter 10y ago

Though unlike Haskell, it is strict.

asattarmd 10y ago
Strict by default. You can make it lazy easily.
clacke2 10y ago
The next Haskell will be strict -- Simon Peyton Jones http://www.cs.nott.ac.uk/%7Egmh/appsem-slides/peytonjones.ppt http://www.cs.nott.ac.uk/%7Egmh/appsem-slides/peytonjones.pp... /via https://news.ycombinator.com/item?id=1924061 https://news.ycombinator.com/item?id=1924061
- kobeya 10y ago
  Yes, but not because laziness was a technical failure, but for something more resembling PR reasons. Haskell's laziness by default ends up being a large stumbling block for many developers not used to thinking in that way. Although I understand why Idris is strict by default, there is a part of me that dies a little from that understanding :(
  - mafribe 10y ago
    The main problem with laziness is that, according to SPJ "[l]aziness makes it much, much harder to reason about performance, especially space."
    - willtim 10y ago
      Of course, lazy-by-default also brings many advantages: http://augustss.blogspot.co.uk/2011/05/more-points-for-lazy-evaluation-in.html http://augustss.blogspot.co.uk/2011/05/more-points-for-lazy-...
      - deleted 10y ago
        [deleted]
  - solidsnack9000 10y ago
    It's not so much a PR failure, as an ergonomics issue -- making laziness the default makes it too easy for people to create performance problems for themselves. Haskell's laziness undoubtedly works and is useful; you might say it was Haskell's strictness that needed improving.
pjmlp 10y ago
Haskell is just lazy by default, you can make code explicitly strict. Just like other languages are strict by default, but can be made lazy via sequences, streams, generators,... It is just a matter which defaults might be better for a given application.
- vram22 10y ago
  What does strict mean in this context? I don't know too much about these concepts. I think lazy means only evaluated when needed, like in generators (using Python as an example, which I know - I don't know Haskell or Idris). And I thought (from what little I've read), that the opposite of lazy evaluation was eager evaluation. So in Python at least, an example of eager vs. lazy would be returning a list vs. returning a generator from a function. For the former (list), the whole list would have to be created/populated and then returned (thereby occupying memory for the duration of its use), whereas for the latter (generator), items from it would only be yielded on demand, e.g. one at a time, when next() is called, or when the generator is iterated over, and so would not use as much memory as needed for the sum of the sizes of the items in the list. So where does strict fit in here? Feel free to point if I've got any of the above wrong. Update: Thanks for the replies, people.
  - chongli 10y ago
    Strict evaluation is a synonym for eager evaluation. In Haskell, the primary mechanism for inducing evaluation is the case expression (if/then/else and pattern matching are syntactic sugar for case). Thunks (lazy expressions) in Haskell are created with let and then forced with case. It's very straightforward at the most basic level, there's just a lot of abstraction built on top of it that can obscure what's going on.
  - laszlokorte 10y ago
    strict is same as eager and non-strict is same as lazy https://wiki.haskell.org/Lazy_vs._non-strict https://wiki.haskell.org/Lazy_vs._non-strict
  - mrkgnao 10y ago
    I wrote this a while back. You might find it of some use. https://news.ycombinator.com/item?id=13907573 https://news.ycombinator.com/item?id=13907573

CJefferson 10y ago

Yes, but it turns out you can do some cool things with dependent types. I always felt, as a C++ programmer, that Haskell was just restricting me, without providing me any real benefits (of course, other people's opinion can vary!) -- on the other hand, Idris provides tools I can see as useful, things like checking at compile time all file handles are correctly opened before use, and closed after use (that's a very simple example, but just one type of thing you can do)

pdexter 10y ago
I'm not sure that is quite a simple example actually. Sounds kind of complex to prove that all file handles are closed after use (how soon after use?) in the general sense, especially when they're opened dynamically. Also, you can already do half of what you described in Haskell. Just require the functions that work over open files to require an Open type which the open function would return.
- lgas 10y ago
  If you search for the "File Management" section in this doc, you can see an example of what he's talking about. https://media.readthedocs.org/pdf/idris/latest/idris.pdf https://media.readthedocs.org/pdf/idris/latest/idris.pdf
- chriswarbo 10y ago
  > Just require the functions that work over open files to require an Open type which the open function would return. Not quite. The problem is that values can be copied (AKA used "non-linearly"), for example: open :: FilePath -> IO Open readFile :: Open -> IO String close :: Open -> IO Closed main = do -- Open a file handle o <- open "/tmp/foo" -- Close "o" c <- close o -- Try reading from "o" s <- readFile o putStr s This program will type-check, since "o" has type "Open", so it's a valid input to "close" and to "readFile". The problem is that the type system has no idea that calling (the IO action returned by) "close o" makes subsequent uses of "o" invalid, even though it still has type "Open". With linear types, we can make "Open" and "Closed" linear. It's a type error to use a linearly-typed value more than once, which rules out the above double-usage of "o :: Open". It's also a type error to create a linearly-typed value and not use it at all; we can use this when designing an API, e.g. to make a function like: withFile :: (Open -> (Closed, a)) -> IO a The only way to call this function is to provide it with a function of type `Open -> (Closed, a)`. If we've encapsulated our implementation details, then the only way to write a function which returns a `Closed` is to have it call `close :: Open -> Close`. Since values of type `Open` can't be re-used, this must either be its argument or the return value of some call, e.g. `readFile :: Open -> (Open, String)` or `writeFile :: String -> Open -> IO Open`, which in turn require an `Open` argument, and so on; forcing a chain of operations, culminating in a `close`.

muraiki 10y ago

Another way to think of it is that types are first class. Here's an example I found of returning a type, although I forget where I found it. It's a version of a sample on the Rust page, but it now handles floats if necessary: https://paste.fedoraproject.org/paste/UTrEje4Czbiq8C0u1oJOnF5M1UNdIGYhyRLivL9gydE= https://paste.fedoraproject.org/paste/UTrEje4Czbiq8C0u1oJOnF...

deleted 10y ago
[deleted]

jadbox 10y ago

Does Scala have this kind of dependent types? What does Idris type system provide that Scala doesn't support?

jackmott 10y ago
no. in idris you can declare a functions that takes integers less than five, and if you write code that can eve theoretically allow that function to get called with 5 or greater you get a compiler error. things like that
virtualwhys 10y ago
Scala has path dependent types. def foo(a: Bar)(b: a.Baz) = ... Idris' dependent types are more powerful, though @edwinb would probably be the one to explain the differences in detail (he gave a talk awhile back on Scala vs. Idris).
lmm 10y ago
Most, possibly all, of what you do in Idris can be encoded into Scala, but working with type-level functions become very cumbersome. The compiler doesn't understand that a type-level function is a function, so every time you apply a function to a type and need to know the result is the same as itself you have to summon evidence that this is so (which also sends compile times through the roof). Higher-kinded types get treated differently for equality unless you encode them as members of wrapper types. You end up having to write all your type-level stuff in a kind of continuation-passing style and defining intermediate types to represent each step of your algorithm.

kemiller2002 10y ago

There are other differences too. The syntax is very very close, but how it handles things like evaluation is different. Don't assume that just because they look the same that they are.