6 ms·

Is this a good thing? What the development process in this post appears to involve is a mostly-mechanical filling in of function definitions to match a pre-give

by voyou 13y ago

Is this a good thing? What the development process in this post appears to involve is a mostly-mechanical filling in of function definitions to match a pre-given type signature; but, if it's mechanical, shouldn't the compiler be able to do it for us?

mightybyte 13y ago
The compiler is doing a lot of it for us. > Thanks to GeneralizedNewtypeDeriving, I got the three instances I wanted for free via F. A good bit of what you're seeing as "mechanical" is actually the simplicity achieved because Haskell is expressive enough to get very close to the abstractions that we really need. Haskell allows you to decompose problems in ways such that each step along the way is very simple and in many cases obviously correct. Obligatory Hoare quote: > There are two ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies. And the other way is to make it so complicated that there are no obvious deficiencies.
astrobe_ 13y ago
Haskell is absolutely fantastic. In C, when I'm given only the prototype of a function like: > int foo(int, int); Even if you tell me it is referentially transparent, I have no idea what that bloody function really does. But with HASKELL, with just the type signature you can write a program that does what you want even though you don't know what the components you used do! Mind/Blown.
- dllthomas 13y ago
  My C functions look more like thing_t *find_thing(thing_index_t, thing_t *things); Where my indices are wrapped in a single-element struct so that I get some type safety. You can write bad code in any language. The Haskell things that I miss most in C are the parametric polymorphism and the structural pattern matching. Even so, I've been able to encode some surprising invariants in my C types (with occasionally a little bit of manual help)...
- MichaelGG 13y ago
  It really is awesome! If you see a value with this type: (bool -> bool) You know it only has 4 possible names, only 4 things it could possibly do: false, true, not, id. (Ignoring infinite recursion or exceptions.) The list functions are a rich place to explain this to people. (a list -> (a -> b) -> b list) If a declared function has this signature, there's only one reasonable thing it is: map. (It could return the last element only, or an empty b list, but those aren't so reasonable.) What about this? (a list -> (a -> bool) -> a) It'd seem it returns the first item from the list that matches the predicate. Possibly the last item. (And an exception if the list is empty or item isn't found.) Other people aren't as impressed by this as I am, though.
  - skybrian 13y ago
    Yes but those are trivial examples. What about a math library? The type signature isn't going to tell you which trig function to apply. I'm a fan of static typing, but this sort of guessing based on type signatures seems like a bad thing, actually. It's like when people use autocomplete in their IDE and pick anything that looks like it might work, instead of reading the documentation (and maybe the source) to understand what they're using. It's understandable with beginners, but for people who should know better it's willful blindness.
    - nightski 13y ago
      It actually can using generic type signatures with constraints. Once you use a concrete type like Int you are severely limiting the expressiveness of the types. Which is fine in some scenarios.
    - gbhn 13y ago
      It reminds me of dimensional analysis in physics. That works really well when the number of possibilities are low and the system as a whole is contained enough and well-constructed enough that there aren't many pitfalls. But everyone knows physicists can't manage factors of 2 and pi. :-)
    - MichaelGG 13y ago
      I'm not suggesting that you decide "which function to use" based off a type signature. But that the type signature provides a lot of useful constraints to help you reason about things. And those examples point out how in some cases, just with the type signature you can determine exactly what the function can do. The examples show the different from non-pure languages or functions, where "someList.Bla()" returns "void" and might have done anything to the list, from removing all items to reversing them, to calling Bla() on each element inside (which in turn might do who-knows-what). True though, without pure functions then the benefits aren't all there.
- BSousa 13y ago
  I Love Haskell but I think sometimes people give it more credit than deserved. So you say > int foo(int, int); Doesn't tell you anything. Ok, you are right! But that code translated to Haskell would be: > foo :: Int -> Int -> Int How does that give you more information about foo than the C code above? Now if you say you use type synonyms in Haskell, I would agree, but you can use typedefs in C as well.
  - nightski 13y ago
    Well it does tell you that there are no IO computations with side effects. So you really are restricted to the Int type and the operations that can be performed on it. You get much stronger statements by using type variables (not type synonyms). This is actually laid out rather clearly in Theorems for Free by Wadler[1]. The essence is that the more generic a type signature gets, the more you can reason about it's behavior. Since if you want to perform (+) (-) (*) (/) for example you'll need to include a (Num) constraint. [1] http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf
    - jlarocco 13y ago
      > So you really are restricted to the Int type and the operations that can be performed on it. That's so vague it's almost meaningless, and doesn't support the original assertion, which was "But with HASKELL, with just the type signature you can write a program that does what you want even though you don't know what the components you used do!" Even given a simple thing like foo:: int -> int -> int, there's really no way to tell what it's doing. It could be multiplying the arguments together, dividing, adding, computing psuedo-random numbers using two seed values, ... Not only that, but I'm not sure it's true that it's limited to the Int type because there are things like System.IO.Unsafe.
      - mightybyte 13y ago
        > Even given a simple thing like foo:: int -> int -> int, there's really no way to tell what it's doing. Ahh, this is an important point. The reason you can't tell what it's doing is because it is quite concrete. One really cool thing about this kind of type system is that the more generic your functions, the more you can tell about what it's doing. Consider this function: foo :: (a, b) -> a There's only one possible thing this function can do! And there's only one possible implementation--the correct one. This is the case because the types involved are completely general. Type signatures can communicate a lot more than one might think.
dllthomas 13y ago
My understanding is that Agda will do it for you. I think GHC is getting something similar with type holes, too.
- freyrs3 13y ago
  Agda has proof search, yes. But for example if you write down the expression for `and` with type holes: and : Bool -> Bool -> Bool and a false = { }0 and a true = { }1 It will deduce the following which is well-typed but not correct. and : Bool -> Bool -> Bool and true false = false and false true = false If the types are precise and highly constrained it works well, but it's imperfect.
  - dllthomas 13y ago
    I think you left out the wrong case (and another right one). Also, while this is the same functionality, it shouldn't really be expected to work well when dealing with concrete types - you're not nearly as constrained as when you have a bunch of polymorphic terms in the relevant type signatures - like was the case in the article here.
- judk 13y ago
  Haskell has Djinn. Not as powerful as Agda.
chowells 13y ago
It's a very good thing that when there's only one way to get the correct result, the compiler forbids everything else. Would you prefer the compiler allow incorrect code?
- judk 13y ago
  All the Python fans say "yes".
  - eru 13y ago
    GHC added that as a feature, recently.
  - drdaeman 13y ago
    Not all. PyCharm has excellent static analysis capabilities for this. One just have to hint it with `assert isinstance(spam, Egg)` on occasions. Catches me tons of bugs before interpreter ever hits them. Which is way nicer than getting an exception notification email with some live customer hitting 500 page because there's a TypeError in some obscure execution path you've never really tested.

by voyou 13y ago

mightybyte 13y ago

The compiler is doing a lot of it for us. > Thanks to GeneralizedNewtypeDeriving, I got the three instances I wanted for free via F. A good bit of what you're seeing as "mechanical" is actually the simplicity achieved because Haskell is expressive enough to get very close to the abstractions that we really need. Haskell allows you to decompose problems in ways such that each step along the way is very simple and in many cases obviously correct. Obligatory Hoare quote: > There are two ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies. And the other way is to make it so complicated that there are no obvious deficiencies.

astrobe_ 13y ago

Haskell is absolutely fantastic. In C, when I'm given only the prototype of a function like: > int foo(int, int); Even if you tell me it is referentially transparent, I have no idea what that bloody function really does. But with HASKELL, with just the type signature you can write a program that does what you want even though you don't know what the components you used do! Mind/Blown.

dllthomas 13y ago
My C functions look more like thing_t *find_thing(thing_index_t, thing_t *things); Where my indices are wrapped in a single-element struct so that I get some type safety. You can write bad code in any language. The Haskell things that I miss most in C are the parametric polymorphism and the structural pattern matching. Even so, I've been able to encode some surprising invariants in my C types (with occasionally a little bit of manual help)...
MichaelGG 13y ago
It really is awesome! If you see a value with this type: (bool -> bool) You know it only has 4 possible names, only 4 things it could possibly do: false, true, not, id. (Ignoring infinite recursion or exceptions.) The list functions are a rich place to explain this to people. (a list -> (a -> b) -> b list) If a declared function has this signature, there's only one reasonable thing it is: map. (It could return the last element only, or an empty b list, but those aren't so reasonable.) What about this? (a list -> (a -> bool) -> a) It'd seem it returns the first item from the list that matches the predicate. Possibly the last item. (And an exception if the list is empty or item isn't found.) Other people aren't as impressed by this as I am, though.
- skybrian 13y ago
  Yes but those are trivial examples. What about a math library? The type signature isn't going to tell you which trig function to apply. I'm a fan of static typing, but this sort of guessing based on type signatures seems like a bad thing, actually. It's like when people use autocomplete in their IDE and pick anything that looks like it might work, instead of reading the documentation (and maybe the source) to understand what they're using. It's understandable with beginners, but for people who should know better it's willful blindness.
  - nightski 13y ago
    It actually can using generic type signatures with constraints. Once you use a concrete type like Int you are severely limiting the expressiveness of the types. Which is fine in some scenarios.
  - gbhn 13y ago
    It reminds me of dimensional analysis in physics. That works really well when the number of possibilities are low and the system as a whole is contained enough and well-constructed enough that there aren't many pitfalls. But everyone knows physicists can't manage factors of 2 and pi. :-)
  - MichaelGG 13y ago
    I'm not suggesting that you decide "which function to use" based off a type signature. But that the type signature provides a lot of useful constraints to help you reason about things. And those examples point out how in some cases, just with the type signature you can determine exactly what the function can do. The examples show the different from non-pure languages or functions, where "someList.Bla()" returns "void" and might have done anything to the list, from removing all items to reversing them, to calling Bla() on each element inside (which in turn might do who-knows-what). True though, without pure functions then the benefits aren't all there.
BSousa 13y ago
I Love Haskell but I think sometimes people give it more credit than deserved. So you say > int foo(int, int); Doesn't tell you anything. Ok, you are right! But that code translated to Haskell would be: > foo :: Int -> Int -> Int How does that give you more information about foo than the C code above? Now if you say you use type synonyms in Haskell, I would agree, but you can use typedefs in C as well.
- nightski 13y ago
  Well it does tell you that there are no IO computations with side effects. So you really are restricted to the Int type and the operations that can be performed on it. You get much stronger statements by using type variables (not type synonyms). This is actually laid out rather clearly in Theorems for Free by Wadler[1]. The essence is that the more generic a type signature gets, the more you can reason about it's behavior. Since if you want to perform (+) (-) (*) (/) for example you'll need to include a (Num) constraint. [1] http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf
  - jlarocco 13y ago
    > So you really are restricted to the Int type and the operations that can be performed on it. That's so vague it's almost meaningless, and doesn't support the original assertion, which was "But with HASKELL, with just the type signature you can write a program that does what you want even though you don't know what the components you used do!" Even given a simple thing like foo:: int -> int -> int, there's really no way to tell what it's doing. It could be multiplying the arguments together, dividing, adding, computing psuedo-random numbers using two seed values, ... Not only that, but I'm not sure it's true that it's limited to the Int type because there are things like System.IO.Unsafe.
    - mightybyte 13y ago
      > Even given a simple thing like foo:: int -> int -> int, there's really no way to tell what it's doing. Ahh, this is an important point. The reason you can't tell what it's doing is because it is quite concrete. One really cool thing about this kind of type system is that the more generic your functions, the more you can tell about what it's doing. Consider this function: foo :: (a, b) -> a There's only one possible thing this function can do! And there's only one possible implementation--the correct one. This is the case because the types involved are completely general. Type signatures can communicate a lot more than one might think.

dllthomas 13y ago

My understanding is that Agda will do it for you. I think GHC is getting something similar with type holes, too.

freyrs3 13y ago
Agda has proof search, yes. But for example if you write down the expression for `and` with type holes: and : Bool -> Bool -> Bool and a false = { }0 and a true = { }1 It will deduce the following which is well-typed but not correct. and : Bool -> Bool -> Bool and true false = false and false true = false If the types are precise and highly constrained it works well, but it's imperfect.
- dllthomas 13y ago
  I think you left out the wrong case (and another right one). Also, while this is the same functionality, it shouldn't really be expected to work well when dealing with concrete types - you're not nearly as constrained as when you have a bunch of polymorphic terms in the relevant type signatures - like was the case in the article here.
judk 13y ago
Haskell has Djinn. Not as powerful as Agda.

chowells 13y ago

It's a very good thing that when there's only one way to get the correct result, the compiler forbids everything else. Would you prefer the compiler allow incorrect code?

judk 13y ago
All the Python fans say "yes".
- eru 13y ago
  GHC added that as a feature, recently.
- drdaeman 13y ago
  Not all. PyCharm has excellent static analysis capabilities for this. One just have to hint it with `assert isinstance(spam, Egg)` on occasions. Catches me tons of bugs before interpreter ever hits them. Which is way nicer than getting an exception notification email with some live customer hitting 500 page because there's a TypeError in some obscure execution path you've never really tested.