Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.


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.


What makes it ill-defined is that it computes infinitely -- that's why you need a totality checker (or a total language).




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: