3 ms·
Given line "loopType : Int -> Type", how can line "loopType x = loopType x" mean anything useful? It should be rejected and ignored as a tautology, leaving loop
by HelloNurse 2y ago
Given line "loopType : Int -> Type", how can line "loopType x = loopType x" mean anything useful? It should be rejected and ignored as a tautology, leaving loopType undefined or defined by default as a distinct unique value for each int.
- remexre 2y agoWhat makes it ill-defined is that it computes infinitely -- that's why you need a totality checker (or a total language).