12 ms·

Errors could presumably be provided as return values (similar to Rust's Option or Haskell's Either), though we know from languages like Go that propagating thes

Errors could presumably be provided as return values (similar to Rust's Option or Haskell's Either), though we know from languages like Go that propagating these manually is a chore and an eyesore. A harder problem is errors that cannot be handled by a simpler type system. For example, consider Haskell's head function, which is defined like this: head :: [a] -> a In other words, it takes a list, and returns the first element. But if the list is empty, it throws an exception (technically called an "error" in Haskell): > head [] *** Exception: Prelude.head: empty list Haskell's type system is extremely powerful, but it cannot catch this at compile time. In order to express constraints such as "list must not be empty" or "number must be higher than 1" or "file must be open, the type system needs to understand the semantics of the values expressed by a type system. This can be solved by dependent typing, but that's a complicated concept currently implemented by only a handful of languages (e.g. Idris).

tylerhou 8y ago
You still can't avoid runtime errors because of non-terminating functions. Determining whether an arbitrary function in a Turing complete language is total or not is undecidable. I don't see any mention of a totality checker (which would make the language not Turing complete) either. Idris also has this.
akegalj 8y ago
> This can be solved by dependent typing dependant typing isn't needed for some use cases you have mentioned: > list must not be empty you can use NonEmpty https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-List-NonEmpty.html https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-L... . We are still encoding this special case and our intent in types. Cons is that we need a special support for it (special library) where with dependant types we could reason about this use case without a special library EDIT: added newlines
masklinn 8y ago
> Errors could presumably be provided as return values (similar to Rust's Option or Haskell's Either), though we know from languages like Go that propagating these manually is a chore and an eyesore. Mostly because Go is terrible. > Haskell's type system is extremely powerful, but it cannot catch this at compile time. The problem is not the type system, it's that Haskell's error handling is inconsistent. Elm, despite having a much simpler type system than Haskell, handles this properly: head : List a -> Maybe a This has nothing to do with the type system itself and everything to do with how the type system is used (or not used). The designers of Haskell's `head` decided to make it a partial function, leading to type-checking inputs not generating any output.
- galaxyLogic 8y ago
  This seems like such an obvious solution it makes me wonder why creators of Haskell did not think of it? Lists are a very basic type used all the time if you don't get that right lot of the value of the great type-system is lost I would think.
  - masklinn 8y ago
    I think it's because they weren't very clear on how they wanted to handle partial functions / error reporting, and historically functions like head are partial. Making them total makes them a bit heavier for the best case, and furthermore can seem unnecessary (as you could just pattern-match the list itself). You can also see this oddity in Haskell allowing non-exhaustive case, and allowing refutable patterns in bindings.
  - lodi 8y ago
    They did. The elm-style version is in the standard libraries as: listToMaybe :: [a] -> Maybe a (http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Maybe.html#v:listToMaybe http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-M...)
    - galaxyLogic 8y ago
      That's a lengthy name for the simple operation of getting the first element of a list if there is one. I would have preferred 'car' :-)
      - lodi 8y ago
        It's a bit verbose, but this kind of thing is far less prevalent in Haskell anyway; most of the time you destructure a list through pattern matching, not explicit head/tail functions.
dragonwriter 8y ago
> A harder problem is errors that cannot be handled by a simpler type system. For example, consider Haskell's head function Haskell's head function is often pointed to as a wart even given Haskell's type system; the signature really ought to be: head :: [a] -> Maybe a With a definition (equivalent to): head [] = None head x:xs = Some x It's absolutely not a good example of a source of errors that can't be dealt with in a type system like Haskell's. > In order to express constraints such as "list must not be empty" or "number must be higher than 1" or "file must be open, the type system needs to understand the semantics of the values expressed by a type system. Sure, but you don't have to express those as type constraints to avoid runtime errors when they occur; if you can express the distinction in normal code you can use distinctions of return type.

tylerhou 8y ago

You still can't avoid runtime errors because of non-terminating functions. Determining whether an arbitrary function in a Turing complete language is total or not is undecidable. I don't see any mention of a totality checker (which would make the language not Turing complete) either. Idris also has this.

akegalj 8y ago

> This can be solved by dependent typing dependant typing isn't needed for some use cases you have mentioned: > list must not be empty you can use NonEmpty https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-List-NonEmpty.html https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-L... . We are still encoding this special case and our intent in types. Cons is that we need a special support for it (special library) where with dependant types we could reason about this use case without a special library EDIT: added newlines

masklinn 8y ago

> Errors could presumably be provided as return values (similar to Rust's Option or Haskell's Either), though we know from languages like Go that propagating these manually is a chore and an eyesore. Mostly because Go is terrible. > Haskell's type system is extremely powerful, but it cannot catch this at compile time. The problem is not the type system, it's that Haskell's error handling is inconsistent. Elm, despite having a much simpler type system than Haskell, handles this properly: head : List a -> Maybe a This has nothing to do with the type system itself and everything to do with how the type system is used (or not used). The designers of Haskell's `head` decided to make it a partial function, leading to type-checking inputs not generating any output.

galaxyLogic 8y ago
This seems like such an obvious solution it makes me wonder why creators of Haskell did not think of it? Lists are a very basic type used all the time if you don't get that right lot of the value of the great type-system is lost I would think.
- masklinn 8y ago
  I think it's because they weren't very clear on how they wanted to handle partial functions / error reporting, and historically functions like head are partial. Making them total makes them a bit heavier for the best case, and furthermore can seem unnecessary (as you could just pattern-match the list itself). You can also see this oddity in Haskell allowing non-exhaustive case, and allowing refutable patterns in bindings.
- lodi 8y ago
  They did. The elm-style version is in the standard libraries as: listToMaybe :: [a] -> Maybe a (http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Maybe.html#v:listToMaybe http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-M...)
  - galaxyLogic 8y ago
    That's a lengthy name for the simple operation of getting the first element of a list if there is one. I would have preferred 'car' :-)
    - lodi 8y ago
      It's a bit verbose, but this kind of thing is far less prevalent in Haskell anyway; most of the time you destructure a list through pattern matching, not explicit head/tail functions.

dragonwriter 8y ago

> A harder problem is errors that cannot be handled by a simpler type system. For example, consider Haskell's head function Haskell's head function is often pointed to as a wart even given Haskell's type system; the signature really ought to be: head :: [a] -> Maybe a With a definition (equivalent to): head [] = None head x:xs = Some x It's absolutely not a good example of a source of errors that can't be dealt with in a type system like Haskell's. > In order to express constraints such as "list must not be empty" or "number must be higher than 1" or "file must be open, the type system needs to understand the semantics of the values expressed by a type system. Sure, but you don't have to express those as type constraints to avoid runtime errors when they occur; if you can express the distinction in normal code you can use distinctions of return type.