DIJamner / InDependent

A gradual, dependently typed language
7 stars 1 forks source link

Verification accepts undefined types in native declarations #6

Closed DIJamner closed 9 years ago

DIJamner commented 9 years ago

Types of terms in a native declaration are assumed to exist. The following declaration is allowed and can be used in other functions.

native myNT : NT

However, this leads to unexpected behavior in situations like the following:

id= \t:{Type1}.\a:t.a
res = (id NT)

In this case, the type of NT is undefined, and so it causes a validation error. If however, NT is declared using the following statement it behaves correctly.

native NT : Type1

This behavior does not compromise validity, but it is important to note for programs making use of JavaScript bindings that use custom types.