5 ms·

"To distinguish between things that have the same interfaces, but also have semantic or other contractual differences, we need types." I don't see that "types"

"To distinguish between things that have the same interfaces, but also have semantic or other contractual differences, we need types." I don't see that "types" solve this problem, as there are far more varieties of function than lazy and eager, which themselves are not always consistent. Perhaps Eiffel is a better guide for the sort of pre-condition / post-condition assumptions of a function, if you want to go down this route. https://en.wikipedia.org/wiki/Eiffel_(programming_language)#Design_by_contract https://en.wikipedia.org/wiki/Eiffel_(programming_language)#...

lmm 11y ago
Contracts that are enforced at compile time are types, whether you call them that or not.
- asQuirreL 11y ago
  Some types are not (and cannot) be enforced at compile time [0]. In fact what makes something a type is not something internal to the type, but its participation in a larger type system or type theory, so in that sense, almost any abstract model of computation could give rise to types, as long as it was sound. [0]: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
  - gergoerdi 11y ago
    Wait what? The whole point of dependetly-typed languages is that programs you write in them are fully typechecked at compile time.
    - asQuirreL 11y ago
      In a dependently typed language, types may rely upon arbitrary terms that are computed at runtime, and yet you are correct that dependently typed programs are checked statically. The way this is achieved is if a property can only be checked at runtime, then the burden of proof for that property is moved from the typechecker to the program. The program must verify the property at runtime and create a witness to the proof, which it can then pass to functions to say that it has done the necessary work. So I guess the answer is yes and no. I would say the whole point of dependently-typed languages is that we can statically determine that somebody is maintaining correctness, be it at compile time or at run time.
- marcosdumay 11y ago
  Contracts are types. If they are enforced at compile time, they are static.
eveningcoffee 11y ago
I think that the problem here is actually in signaling a wrong interface. If you in fact want to receive a iterable, then you should not signal that you expect a list. The keyword yield is in fact a nice language integrated mechanism to create a iterable interface. In languages that lacking this it resorts to using much more verbose mechanism.

lmm 11y ago

Contracts that are enforced at compile time are types, whether you call them that or not.

asQuirreL 11y ago
Some types are not (and cannot) be enforced at compile time [0]. In fact what makes something a type is not something internal to the type, but its participation in a larger type system or type theory, so in that sense, almost any abstract model of computation could give rise to types, as long as it was sound. [0]: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
- gergoerdi 11y ago
  Wait what? The whole point of dependetly-typed languages is that programs you write in them are fully typechecked at compile time.
  - asQuirreL 11y ago
    In a dependently typed language, types may rely upon arbitrary terms that are computed at runtime, and yet you are correct that dependently typed programs are checked statically. The way this is achieved is if a property can only be checked at runtime, then the burden of proof for that property is moved from the typechecker to the program. The program must verify the property at runtime and create a witness to the proof, which it can then pass to functions to say that it has done the necessary work. So I guess the answer is yes and no. I would say the whole point of dependently-typed languages is that we can statically determine that somebody is maintaining correctness, be it at compile time or at run time.
marcosdumay 11y ago
Contracts are types. If they are enforced at compile time, they are static.

eveningcoffee 11y ago

I think that the problem here is actually in signaling a wrong interface. If you in fact want to receive a iterable, then you should not signal that you expect a list. The keyword yield is in fact a nice language integrated mechanism to create a iterable interface. In languages that lacking this it resorts to using much more verbose mechanism.