6 ms·

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 provi

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`.
  - pdexter 10y ago
    I said half.
    - chriswarbo 10y ago
      Yes, but your approach doesn't actually solve any of the requirements: > things like checking at compile time all file handles are correctly opened before use, and closed after use Using distinct `Open` and `Closed` types, as you say, doesn't help at all with ensuring file handles are closed after use. They also don't ensure that handles are correctly opened before use, as I showed with my example `open "/tmp/foo" >>= (\o -> close o >> readFile o >>= putStr)`. I can't think of a way to ensure both of these things, without using linear or dependent types to track state machines in types. I can think of ways to ensure one of these things: - To ensure files are correctly opened, we can remove the ability to close them. My above example would then work correctly, since `close o` would be a no-op, and `readFile` would succeed. - To ensure all handles get closed, we can remove the ability to open them. Separating handles into `Open` and `Closed` varieties does nothing more than provide documentation hints to programmers; it cannot automatically check whether handles are used correctly, it requires programmers to consciously avoid language features (like using variables multiple times), be careful about the way they compose functions, and write test suites to check if things are working. In other words, it provides none of the benefits of static typing, and is more akin to documentation in a dynamically typed language.
tuukkah 10y ago
Your example (and more) can be achieved by linear types which are coming to Haskell: "The patch is currently under 1000 lines long. We are targeting a merge by the time of the 8.4 release of GHC." http://blog.tweag.io/posts/2017-03-13-linear-types.html http://blog.tweag.io/posts/2017-03-13-linear-types.html
- riffraff 10y ago
  As I understand it, one selling point of Idris' type system is that it's actually simpler than haskell as it's based on a single very generic concept that covers a wide range of applications, rather than a sum of specialized things. There was some discussion previously on HN about this https://news.ycombinator.com/item?id=12350273 https://news.ycombinator.com/item?id=12350273
  - tathougies 10y ago
    But type inference takes a hit. Trade offs -- conceptually similar but potentially needing more annotation
    - mietek 10y ago
      Good Haskell style already presupposes top-level type annotations.
      - bad_user 10y ago
        Highly generic code yields complicated signatures, so even if it's good style to add those signatures for top level declarations, it's really good to have the compiler help you figure out what that signature is.
    - ziman 10y ago
      While dependent type inference is more difficult, you get program inference in exchange. That's not a bad tradeoff because I'd rather write the spec (type) and have the computer fill in the boring bits, rather than the other way around.
masklinn 10y ago
> 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) AFAIK that sounds like unique/linear types, which Idris doesn't provide at this point, it's an experimental/work in progress feature: http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...
- edwinb 10y ago
  Tracking state (sort of like Typestate) is not part of the type system, but you can encode it in the type system. So far, I've found this much more usable in practice than linear types, but I expect future work on linear types will change this, especially now that they're coming to GHC. There's a tutorial on just this sort of thing here: http://docs.idris-lang.org/en/latest/st/index.html http://docs.idris-lang.org/en/latest/st/index.html
snaky 10y ago
Being a C++ programmer, you would like the ATS programming language https://bluishcoder.co.nz/tags/ats/index.html https://bluishcoder.co.nz/tags/ats/index.html
- Buttons840 10y ago
  There seem to be very few resources for learning ATS. How would you suggest learning it?
Too 10y ago
C++ (if not used as C with classes) is built around RAII and will also enforce file handles to be opened before use and automatically closed when leaving scope (no longer in use). See https://github.com/isocpp/CppCoreGuidelines/blob/master/CppCoreGuidelines.md#Rp-leak https://github.com/isocpp/CppCoreGuidelines/blob/master/CppC...
- lkitching 10y ago
  This isn't the same thing - Idris encodes the state machine in the type system, C++ enforces it dynamically.
  - Too 10y ago
    Now std::ifstream isn't 100% idiomatic RAII (because constructor sets error state instead of throwing and it also provides open/close-methods) but generally you should be able to encode a safe file handle into the c++ type system. Here is how i would compare it to what idris describes in https://media.readthedocs.org/pdf/idris/latest/idris.pdf https://media.readthedocs.org/pdf/idris/latest/idris.pdf * It is necessary to open a file for reading before reading it > Enforced by RAII, create file handle(variable) is equivalent to opening file * Opening may fail, so the programmer should check whether opening was successful > If opening file fails, exception is thrown when the handle is created, it is impossible to create/use an unopened handle. * A file which is open for reading must not be written to, and vice versa > Can be enforced with different types for reading and writing (ifstream vs ofstream). * When finished, an open file handle should be closed > fstream is automatically closed when variable goes out of scope. * When a file is closed, its handle should no longer be used > Here it's actually the other way around, the correct way to close a file is to get rid of the last handle refering to it. > Hence a handle can't be used to write to a closed file since such a handle cannot exist in the first place.
    - lmm 10y ago
      > If opening file fails, exception is thrown when the handle is created, it is impossible to create/use an unopened handle. Unfortunately C++ offers no way to track which exceptions any given function might throw and/or enforce that they are handled. > fstream is automatically closed when variable goes out of scope. That works for the simple case where the variable exists on the stack of a single function. C++ does not offer safety in the general case where you pass a handle to/from functions, store it in data structures and so on. (You have the option of runtime checks via shared_ptr etc, but at that point you have very little assurance the file ever actually gets closed).

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`.
- pdexter 10y ago
  I said half.
  - chriswarbo 10y ago
    Yes, but your approach doesn't actually solve any of the requirements: > things like checking at compile time all file handles are correctly opened before use, and closed after use Using distinct `Open` and `Closed` types, as you say, doesn't help at all with ensuring file handles are closed after use. They also don't ensure that handles are correctly opened before use, as I showed with my example `open "/tmp/foo" >>= (\o -> close o >> readFile o >>= putStr)`. I can't think of a way to ensure both of these things, without using linear or dependent types to track state machines in types. I can think of ways to ensure one of these things: - To ensure files are correctly opened, we can remove the ability to close them. My above example would then work correctly, since `close o` would be a no-op, and `readFile` would succeed. - To ensure all handles get closed, we can remove the ability to open them. Separating handles into `Open` and `Closed` varieties does nothing more than provide documentation hints to programmers; it cannot automatically check whether handles are used correctly, it requires programmers to consciously avoid language features (like using variables multiple times), be careful about the way they compose functions, and write test suites to check if things are working. In other words, it provides none of the benefits of static typing, and is more akin to documentation in a dynamically typed language.

tuukkah 10y ago

Your example (and more) can be achieved by linear types which are coming to Haskell: "The patch is currently under 1000 lines long. We are targeting a merge by the time of the 8.4 release of GHC." http://blog.tweag.io/posts/2017-03-13-linear-types.html http://blog.tweag.io/posts/2017-03-13-linear-types.html

riffraff 10y ago
As I understand it, one selling point of Idris' type system is that it's actually simpler than haskell as it's based on a single very generic concept that covers a wide range of applications, rather than a sum of specialized things. There was some discussion previously on HN about this https://news.ycombinator.com/item?id=12350273 https://news.ycombinator.com/item?id=12350273
- tathougies 10y ago
  But type inference takes a hit. Trade offs -- conceptually similar but potentially needing more annotation
  - mietek 10y ago
    Good Haskell style already presupposes top-level type annotations.
    - bad_user 10y ago
      Highly generic code yields complicated signatures, so even if it's good style to add those signatures for top level declarations, it's really good to have the compiler help you figure out what that signature is.
  - ziman 10y ago
    While dependent type inference is more difficult, you get program inference in exchange. That's not a bad tradeoff because I'd rather write the spec (type) and have the computer fill in the boring bits, rather than the other way around.

masklinn 10y ago

> 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) AFAIK that sounds like unique/linear types, which Idris doesn't provide at this point, it's an experimental/work in progress feature: http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...

edwinb 10y ago
Tracking state (sort of like Typestate) is not part of the type system, but you can encode it in the type system. So far, I've found this much more usable in practice than linear types, but I expect future work on linear types will change this, especially now that they're coming to GHC. There's a tutorial on just this sort of thing here: http://docs.idris-lang.org/en/latest/st/index.html http://docs.idris-lang.org/en/latest/st/index.html

snaky 10y ago

Being a C++ programmer, you would like the ATS programming language https://bluishcoder.co.nz/tags/ats/index.html https://bluishcoder.co.nz/tags/ats/index.html

Buttons840 10y ago
There seem to be very few resources for learning ATS. How would you suggest learning it?

Too 10y ago

C++ (if not used as C with classes) is built around RAII and will also enforce file handles to be opened before use and automatically closed when leaving scope (no longer in use). See https://github.com/isocpp/CppCoreGuidelines/blob/master/CppCoreGuidelines.md#Rp-leak https://github.com/isocpp/CppCoreGuidelines/blob/master/CppC...

lkitching 10y ago
This isn't the same thing - Idris encodes the state machine in the type system, C++ enforces it dynamically.
- Too 10y ago
  Now std::ifstream isn't 100% idiomatic RAII (because constructor sets error state instead of throwing and it also provides open/close-methods) but generally you should be able to encode a safe file handle into the c++ type system. Here is how i would compare it to what idris describes in https://media.readthedocs.org/pdf/idris/latest/idris.pdf https://media.readthedocs.org/pdf/idris/latest/idris.pdf * It is necessary to open a file for reading before reading it > Enforced by RAII, create file handle(variable) is equivalent to opening file * Opening may fail, so the programmer should check whether opening was successful > If opening file fails, exception is thrown when the handle is created, it is impossible to create/use an unopened handle. * A file which is open for reading must not be written to, and vice versa > Can be enforced with different types for reading and writing (ifstream vs ofstream). * When finished, an open file handle should be closed > fstream is automatically closed when variable goes out of scope. * When a file is closed, its handle should no longer be used > Here it's actually the other way around, the correct way to close a file is to get rid of the last handle refering to it. > Hence a handle can't be used to write to a closed file since such a handle cannot exist in the first place.
  - lmm 10y ago
    > If opening file fails, exception is thrown when the handle is created, it is impossible to create/use an unopened handle. Unfortunately C++ offers no way to track which exceptions any given function might throw and/or enforce that they are handled. > fstream is automatically closed when variable goes out of scope. That works for the simple case where the variable exists on the stack of a single function. C++ does not offer safety in the general case where you pass a handle to/from functions, store it in data structures and so on. (You have the option of runtime checks via shared_ptr etc, but at that point you have very little assurance the file ever actually gets closed).