3 ms·

Type inference does not automatically "typify" your code. The type system -- whether the type annotations are explicit or the types are inferred -- determines w

by pron 7y ago

Type inference does not automatically "typify" your code. The type system -- whether the type annotations are explicit or the types are inferred -- determines which expressions are "well-formed" (i.e. syntactically correct), and so you can't write arbitrary code. E.g., in Haskell, you can know for a fact that at one call site a Maybe instance is Just, but whether you annotate your types or rely on inference, the type system will still force you to match on the constructor even though you don't really have to from a correctness perspective.

PhineasRex 7y ago
If you're talking about the fact that you have to unbox the Maybe, that's not really related to type inference or static types but how "null" values are represented in the language. If you're talking about exhaustiveness checks, you can disable those and use `-fdefer-type-errors` to compile programs which don't type-check. Although I will say that most of the time when you have a Maybe instance that you know is Just, it means you're branching in the wrong part of your program.
- pron 7y ago
  > If you're talking about exhaustiveness checks, you can disable those and use `-fdefer-type-errors` to compile programs which don't type-check. Right, but if you were using, say, Idris, the program would type check. It's just that Haskell's type system is too weak. Disabling type checking is not what the question was about. The program is type-correct, yet not in Haskell's particular system. > Although I will say that most of the time when you have a Maybe instance that you know is Just, it means you're branching in the wrong part of your program. Perhaps, but that doesn't change the fact that if you write it in some way that is perfectly correct, Haskell's particular type system will still not accept your program.
firethief 7y ago
If the reason you know your Maybe T is a Just _ is that you tested it locally: in any language that favors the Maybe pattern, the idiomatic way of performing that test makes the result available to the type system (destructuring / combinators / 'nads). On the other hand, if you know your Maybe is a Just because of non-local information, you will eventually turn out to be wrong :)
- pron 7y ago
  No, you can know -- and even prove -- that at a certain callsite, a Maybe would be a Just, and if you were using a dependent type system, you can prove that in the type system (although it probably won't be automatically inferred -- you may have to work hard for the proof), but Haskell's type system is too weak to express such properties and such proofs, at least in the general case.

by pron 7y ago

PhineasRex 7y ago

If you're talking about the fact that you have to unbox the Maybe, that's not really related to type inference or static types but how "null" values are represented in the language. If you're talking about exhaustiveness checks, you can disable those and use `-fdefer-type-errors` to compile programs which don't type-check. Although I will say that most of the time when you have a Maybe instance that you know is Just, it means you're branching in the wrong part of your program.

pron 7y ago
> If you're talking about exhaustiveness checks, you can disable those and use `-fdefer-type-errors` to compile programs which don't type-check. Right, but if you were using, say, Idris, the program would type check. It's just that Haskell's type system is too weak. Disabling type checking is not what the question was about. The program is type-correct, yet not in Haskell's particular system. > Although I will say that most of the time when you have a Maybe instance that you know is Just, it means you're branching in the wrong part of your program. Perhaps, but that doesn't change the fact that if you write it in some way that is perfectly correct, Haskell's particular type system will still not accept your program.

firethief 7y ago

If the reason you know your Maybe T is a Just _ is that you tested it locally: in any language that favors the Maybe pattern, the idiomatic way of performing that test makes the result available to the type system (destructuring / combinators / 'nads). On the other hand, if you know your Maybe is a Just because of non-local information, you will eventually turn out to be wrong :)

pron 7y ago
No, you can know -- and even prove -- that at a certain callsite, a Maybe would be a Just, and if you were using a dependent type system, you can prove that in the type system (although it probably won't be automatically inferred -- you may have to work hard for the proof), but Haskell's type system is too weak to express such properties and such proofs, at least in the general case.