Jason (jcreed) wrote,

Well, a good reason for a test case to fail is that the test case is wrong.

The trouble with writing good test cases for this type theory is that the ones that create general enough unification problems to be interesting require (as far as I can tell) fifth-order signatures to be typechecked. Or maybe it's fourth; what would you call a signature with a type family in it like
c : ({a:world} (({b:world} ((t -o t) -> t) -> t) -> t)) -> type.
My brain already becomes mushy at about three and a half levels of functional left-hand-side nesting, so it is complete purée now.

Hey, I can get it down by one order after all:
c : ({a:w} (({b:w} (t @ p -> t @ q) -> t) -> t)) -> type
exhibits enough unificational generality, and it's almost something I can make sense of: a type family indexed by a sort of strong double-negation of a refinement of the type t -> t. Maybe with a merely half-mushy brain I can make some progress now...
Tags: work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded