2 ms·

I agree it's better, you will get a compiler warning about a partial function. I did actually mean worse though. The GP at least to me implied that Haskell (for

I agree it's better, you will get a compiler warning about a partial function. I did actually mean worse though. The GP at least to me implied that Haskell (for cases like this) sits in the lowlands between Idris (and other dependently-typed languages) and dynamically-typed languages. Idris deals with the problem "the right way" by helping you guarantee that you deal with dynamic objects in a compile-time-guaranteed safe way, at the cost of some hassle of proving it is. Dynamically-typed languages deal with the problem "the practical way" by letting you pretend its safe so you don't have to go through the hassle of proving it is, at the cost of runtime safety. I think Haskell can also let you do this, it just feels wrong to do it as a Haskell programmer.

chriswarbo 10y ago
You're absolutely right that various hacks can be employed in Haskell; as well as missing branches, we can also exploit laziness to provide "undefined" or "loop = loop" expressions which, if we're right, won't ever be evaluated. I didn't mean to imply that dynamic languages are "better" because they allow unchecked combinations of everything with everything else. Although I also didn't mean to imply that they're strictly "worse", precisely because there are things we can express easily in dynamic languages which take effort to reproduce in something like Haskell. My main reason to mention dynamic languages was as motivation for why you might want to write such code in the first place: using dependent types to, say, prove Euclid's theorem of the infinitude of primes, would probably not motivate many software developers to give Idris a try. Examples like the type-safe printf mentioned in a sibling comment would presumably be much better motivators: we compute a type based on the format string, so providing a string like "Hello world %f %s !" will produce a type `Float -> String -> String` which accepts the required Float and String parameters, then returns the resulting String.
- clusmore 10y ago
  Thanks for clarifying. Off-topic, but related to undefined in Haskell, I love holes in Idris as a way to represent incomplete programs. I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?". You type it in, the program keeps going and a unit test is generated and put away somewhere for you to make sure that later when you implement it, you can help verify that you're doing it right.
  - chriswarbo 10y ago
    Heh, nice idea. Seems a long way off though. GHC semi-recently took a baby step in this direction by adding PartialTypeSignatures, although it emits a warning if you actually use them! This makes sense on its own, but seems a bit silly when we consider that completely removing the signature will fix the warning ;)
  - dllthomas 10y ago
    > I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?" For some cases, this is pretty simple to implement with unsafePerformIO - I've done that once or twice. Not a sin at all in development.
    - clusmore 10y ago
      I hadn't through of doing that, good idea.

chriswarbo 10y ago

You're absolutely right that various hacks can be employed in Haskell; as well as missing branches, we can also exploit laziness to provide "undefined" or "loop = loop" expressions which, if we're right, won't ever be evaluated. I didn't mean to imply that dynamic languages are "better" because they allow unchecked combinations of everything with everything else. Although I also didn't mean to imply that they're strictly "worse", precisely because there are things we can express easily in dynamic languages which take effort to reproduce in something like Haskell. My main reason to mention dynamic languages was as motivation for why you might want to write such code in the first place: using dependent types to, say, prove Euclid's theorem of the infinitude of primes, would probably not motivate many software developers to give Idris a try. Examples like the type-safe printf mentioned in a sibling comment would presumably be much better motivators: we compute a type based on the format string, so providing a string like "Hello world %f %s !" will produce a type `Float -> String -> String` which accepts the required Float and String parameters, then returns the resulting String.

clusmore 10y ago
Thanks for clarifying. Off-topic, but related to undefined in Haskell, I love holes in Idris as a way to represent incomplete programs. I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?". You type it in, the program keeps going and a unit test is generated and put away somewhere for you to make sure that later when you implement it, you can help verify that you're doing it right.
- chriswarbo 10y ago
  Heh, nice idea. Seems a long way off though. GHC semi-recently took a baby step in this direction by adding PartialTypeSignatures, although it emits a warning if you actually use them! This makes sense on its own, but seems a bit silly when we consider that completely removing the signature will fix the warning ;)
- dllthomas 10y ago
  > I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?" For some cases, this is pretty simple to implement with unsafePerformIO - I've done that once or twice. Not a sin at all in development.
  - clusmore 10y ago
    I hadn't through of doing that, good idea.