| 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051 |
- %include lhs2TeX.fmt
- %if anyMath
- %format . = ".~"
- %format alpha = "\alpha"
- %format beta = "\beta"
- %format gamma = "\gamma"
- %format delta = "\delta"
- %format phi = "\phi"
- %format psi = "\psi"
- %format Set = "\SET"
- %format |- = "\vdash"
- %format ? = "~{?}"
- %format when = "\mathbf{when}"
- %endif
- %However, when adding meta-variables things get more complicated.
- %The convertibility of $A$ and $B$ might now be unknown until some of the meta
- %variables have been instantiated.We will give an example illustrating the problem. Given
- %the set of natural numbers, |Nat|, and the set of booleans, |Bool|. Given also a function, |F : Bool -> Set|. The problem we consider is checking if the term
- %|\g. g 0| has type|((x : F ?) -> F (not x)) -> Nat|
- %, where the term |?| is a meta-variable of type |Bool| and |0| is a natural number. We now get the constraints |F ? = Bool|, |F ? = Nat|,
- % and |F (not 0) = Nat|. We can now see that we have a problem since |F (not 0)|
- % is ill-typed.
- When adding meta-variables equality checking gets more complicated, since we cannot
- always decide the validity of an equality, and we may be forced to keep it as a
- constraint. This is well-known in higher order
- unification\cite{huet:unification}: the constraint $?~0 = 0$ has two solutions
- $? = \lambda x.x$ and $? = \lambda x.0$. This appears also in type theory with
- constraints of the form |F ? = Bool| where $F$ is defined by computation rules.
- The fact that we type check modulo yet unsolved constraints can lead to
- ill-typed terms.
- For instance,
- consider the type-checking problem
- |\g. g 0:((x : F ?) -> F (not x)) -> Nat|\footnote{The notation |(x:A) -> B x| should be read as $\forall x:A. B ~x$.}
- where the term ? is a meta-variable of type |Bool|, |0:Nat|, and |F:Bool->Set| where |F false = Nat| and |F true = Bool|.
- First we check that |((x : F ?) -> F (not x)) -> Nat| is a well-formed type, which
- generates the constraint |F ? = Bool|, since the term |not x| forces |x| to be
- of type |Bool|. Checking |\g.g 0| against the type |((x : F ?) -> F (not x)) -> Nat|
- generate then the constraints |F ? = Nat| and then |F (not 0) = Nat|, which contains
- an ill-typed term\footnote{In fact we will also get the constraint |Bool = Bool| which is trivially
- valid and therefore left out.}.
|
