3 ms·
The infinite loop case is: loopType : Int -> Type loopType x = loopType x foo : List (loopType 3) -> Int foo _ = 42 bar : List (loopType
by remexre 2y ago
The 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).