6 ms·

I've never written Haskell but I'm a Agda programmer (a Haskell dialect with dependent types) and I almost always put all the types and don't rely on type infer

I've never written Haskell but I'm a Agda programmer (a Haskell dialect with dependent types) and I almost always put all the types and don't rely on type inference. The obvious exception is if something quick like a = b otherwise I'd always do a : Some -> Type -> MoreType a = f b Readability is a reason why. Types are extremely pedagogic tools. I believe when I think about my code, I just think about types. I don't think about computation, just the topology of types. Can I go to Int from X. If not why? This is very different than when I write Python code. So seeing types in code helps me a lot understand what's going on. But the real reason is: errors. It's so much more easier to understand errors when types are explicit.

kccqzy 6y ago
Agda doesn't have HM-style type inference. Furthermore many times the type is the main content of the program, not so much the value.
- gnulinux 6y ago
  This is true, I should have mentioned it, although my point still applies to HM style type inference as well.
  - cannabis_sam 6y ago
    To a point at least, HM type inference is decidable, but type inference in haskell with certain extensions or in agda (at least with certain pragmas) is not. The possibility of a diverging type-level function would require the type inference algorithm to solve the halting problem. (As I understand it at least, been a while since I got into the details)
bjourne 6y ago
Python has optional typing though.
- Groxx 6y ago
  Python has optional type hinting for optional static analysis tools (e.g. mypy). Types aren't checked at runtime.
  - bjourne 6y ago
    The terminology I used was correct. Python has optional typing. What you are thinking of is gradual typing which Python lacks. See "Is Sound Gradual Typing Dead?" for a description on what the differences are.
    - Groxx 6y ago
      If you pass a string-typed var to a func with an int-typed parameter, it will not fail at runtime. `python the_file.py` will not even emit a warning, much less a failure, because there's absolutely no runtime difference between "has types" and "does not". That's not optional typing. It's just a standardized magic comment (which the reference implementation ignores). It's far from useless, but it's not adding typing to the language.
      - bjourne 6y ago
        Yes, that is "optional typing." Read the article I referenced.
        Groxx 6y ago
        That appears to be a doc about Racket, which it implies does have run-time checks, from the third sentence here: >In particular, Typed Racket’s run-time system remains largely untyped. As a result, even the completely typed configurations of our benchmarks usually import constants, functions, and classes from an untyped module in the run-time system. When these values cross this boundary at run-time, the contract system performs checks, and that imposes additional costs. But I haven't read the whole thing. It doesn't appear to be very related - it seems to be about gradual typing in a language that does run-time checks (with ways to disable them for performance purposes). Typed python has no additional checks than untyped. So it's still untyped. You wouldn't claim my "// int" comments add optional typing to JavaScript, would you? --- edit: here, take it from the source instead: https://docs.python.org/3/library/typing.html https://docs.python.org/3/library/typing.html Note the title is "support for type hints" and this prominent note is right at the top: >Note: The Python runtime does not enforce function and variable type annotations. They can be used by third party tools such as type checkers, IDEs, linters, etc.
mijoharas 6y ago
so, I'm curious, do you write the type of the function first? When I used to write haskell, I'd very often write a function, iterate on it until it did what I want, then infer the type of the function and insert that into the program. Now, I was relatively new to haskell, so was probably less comfortable writing types than reading them (so I assume it was nicer to have the compiler do that for me, eyeball it to check it's what I meant to do, and put it in). I'm wondering if someone more familiar would think "alright, what type do I want my function to be", fill that in, and then write the type out? I definitely agree that a program is more readable with types, which is why I always filled them in (I just did it afterwards!)
- eru 6y ago
  I do both in Haskell. Sometimes I write the types first and sometimes I write the function first. Usually, the functions with more imperative flavour get their implementation first, and the more functionally flavoured bits get their type first. But that's not always the case. Sometimes I even write the QuickCheck properties first.
- deleted 6y ago
  [deleted]
- gnulinux 6y ago
  Again, can't speak for haskell. In agda you usually have 2 goals creating a function * Proving a property of some other object. In this case you have to write the type first since type is the theorem you want to prove, and implementation is the proof. * Implement a transformation. In this case, as you described you might get away first writing the impl, and then the type, but I personally never even attempt to do that since writing out the type gives me a lot to think about the implementation of the transformation. Once types are explicit, implementation usually ends up being a lot more obvious.

kccqzy 6y ago

Agda doesn't have HM-style type inference. Furthermore many times the type is the main content of the program, not so much the value.

gnulinux 6y ago
This is true, I should have mentioned it, although my point still applies to HM style type inference as well.
- cannabis_sam 6y ago
  To a point at least, HM type inference is decidable, but type inference in haskell with certain extensions or in agda (at least with certain pragmas) is not. The possibility of a diverging type-level function would require the type inference algorithm to solve the halting problem. (As I understand it at least, been a while since I got into the details)

bjourne 6y ago

Python has optional typing though.

Groxx 6y ago
Python has optional type hinting for optional static analysis tools (e.g. mypy). Types aren't checked at runtime.
- bjourne 6y ago
  The terminology I used was correct. Python has optional typing. What you are thinking of is gradual typing which Python lacks. See "Is Sound Gradual Typing Dead?" for a description on what the differences are.
  - Groxx 6y ago
    If you pass a string-typed var to a func with an int-typed parameter, it will not fail at runtime. `python the_file.py` will not even emit a warning, much less a failure, because there's absolutely no runtime difference between "has types" and "does not". That's not optional typing. It's just a standardized magic comment (which the reference implementation ignores). It's far from useless, but it's not adding typing to the language.
    - bjourne 6y ago
      Yes, that is "optional typing." Read the article I referenced.
      - Groxx 6y ago
        That appears to be a doc about Racket, which it implies does have run-time checks, from the third sentence here: >In particular, Typed Racket’s run-time system remains largely untyped. As a result, even the completely typed configurations of our benchmarks usually import constants, functions, and classes from an untyped module in the run-time system. When these values cross this boundary at run-time, the contract system performs checks, and that imposes additional costs. But I haven't read the whole thing. It doesn't appear to be very related - it seems to be about gradual typing in a language that does run-time checks (with ways to disable them for performance purposes). Typed python has no additional checks than untyped. So it's still untyped. You wouldn't claim my "// int" comments add optional typing to JavaScript, would you? --- edit: here, take it from the source instead: https://docs.python.org/3/library/typing.html https://docs.python.org/3/library/typing.html Note the title is "support for type hints" and this prominent note is right at the top: >Note: The Python runtime does not enforce function and variable type annotations. They can be used by third party tools such as type checkers, IDEs, linters, etc.

mijoharas 6y ago

so, I'm curious, do you write the type of the function first? When I used to write haskell, I'd very often write a function, iterate on it until it did what I want, then infer the type of the function and insert that into the program. Now, I was relatively new to haskell, so was probably less comfortable writing types than reading them (so I assume it was nicer to have the compiler do that for me, eyeball it to check it's what I meant to do, and put it in). I'm wondering if someone more familiar would think "alright, what type do I want my function to be", fill that in, and then write the type out? I definitely agree that a program is more readable with types, which is why I always filled them in (I just did it afterwards!)

eru 6y ago
I do both in Haskell. Sometimes I write the types first and sometimes I write the function first. Usually, the functions with more imperative flavour get their implementation first, and the more functionally flavoured bits get their type first. But that's not always the case. Sometimes I even write the QuickCheck properties first.
deleted 6y ago
[deleted]
gnulinux 6y ago
Again, can't speak for haskell. In agda you usually have 2 goals creating a function * Proving a property of some other object. In this case you have to write the type first since type is the theorem you want to prove, and implementation is the proof. * Implement a transformation. In this case, as you described you might get away first writing the impl, and then the type, but I personally never even attempt to do that since writing out the type gives me a lot to think about the implementation of the transformation. Once types are explicit, implementation usually ends up being a lot more obvious.