3 ms·
Uhh, endless recursion doesn't cause your typechecker to run indefinitely; all recursion is sort of "endless" from a type perspective, since the recursion only
by aSanchezStern 2y ago
Uhh, endless recursion doesn't cause your typechecker to run indefinitely; all recursion is sort of "endless" from a type perspective, since the recursion only hits a base case based on values. The problem with non-well-founded recursion like `main = main` is that it prevents you from soundly using types as propositions, since you can trivially inhabit any type.
- remexre 2y agoThe infinite loop case is: loopType : Int -> Type loopType x = loopType x foo : List (loopType 3) -> Int foo _ = 42 bar : List (loopType 4) bar = [] baz : Int baz = foo bar Determining if baz type-checks requires evaluating loopType 3 and loopType 4 to determine if they're equal.
- HelloNurse 2y agoGiven 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).