3 ms·
An example: > y = [1] ++ [2] ;; Assume types List[Int], List[Int] > y[0] ;; This should return Union[Int, None] > y[0] + 3 ;; This should fail type-checking
by ywei3410 6y ago
An example:
> y = [1] ++ [2] ;; Assume types List[Int], List[Int]
> y[0] ;; This should return Union[Int, None]
> y[0] + 3 ;; This should fail type-checking
You /know/ the list isn't empty. Sure you can argue that /maybe/ we should be using NonEmptyList, but now imagine this code.
> y = [1, 2] ;; NonEmptyList[Int]
> y = (filter (lambda x: x % 2 == 1) y) ;; Has to return List[Int]
> y[0] ;; Union[Int, None]
Again, we hit into type issues.
- iso8859-1 6y agoThe type system is a proof system. In your examples, the types do not imply the invariants that you want. Does this mean that the type system is faulty? No! It just means that you need to e.g. get a more expressive type system, document code properly, use smart constructors. There are many tools. Nobody said you can trivially prove everything using type systems. So what are your examples showing? I see your code, but I don't know what you're actually trying to do. One interpretation could be, that you want to prove that for the naturals (excluding 0), up to and including 2, there is an odd number. Can one prove this using type systems? Definitely. If you read Software Foundations, you will know how.
- ywei3410 6y agoSure - but the point is that there are /diminishing returns/ on type-systems. The question is then, /where/ should one draw the line when trying to prove certain properties of code; which properties are worthwhile proving? Are you /seriously/ suggesting that one should use Agda or Coq for most code? EDIT. The original comment was suggesting as though dynamic and static type-systems are a dichotomy. I was pointing out that it is a sliding scale from nominally-typed ala Go, all the way to dependently-typed languages; and that's not even including model-checkers!