Dependent Type Theory in Abstract Syntax

[Shashank Pathak]

Hi everyone!

I am going through Aarne's 2004 paper on GF (here), and trying to reproduce the code. I have the following abstract syntax:

abstract DepType = {
    cat
        Set ;
        El Set ;
    data
        Sigma : (A : Set) -> (El A -> Set) -> Set ;
        pair : (A : Set) -> (B : El A -> Set) -> (a : El A) -> El (B a) -> El (Sigma A B) ;
        p : (A : Set) -> (B : El A -> Set) -> El (Sigma A B) -> El A ;
        q : (A : Set) -> (B : El A -> Set) -> (c : El (Sigma A B)) -> El (B (p A B c)) ;
       
    def
        p _ _ (pair _ _ a _) = a ; -- Error
        q _ _ (pair _ _ _ b) = b ; -- Error
   
    fun
        -- Lexicon
        P : Set ;
}

I get an error where I define p and q. Am I doing something wrong? Or might it be that support for higher order types has been stripped down in some way in the newer versions of GF? Thank you.

[Hans Leiss]

Hi Shashank,

you cannot introduce p and q as constructors by "data" and *also*
provide equations for them by "def". So, you have to introduce p,q by
fun-declarations and can then provide def-computation rules. For

fun p : (A : Set) -> (B : El A -> Set) -> El (Sigma A B) -> El A ;

def p _ _ (pair _ _ a _) = a ;

this is ok, and the compiler accepts it. But for q, with

fun q : (A : Set) -> (B : El A -> Set) -> (c : El (Sigma A B)) -> El (B (p A B c)) ;
def q A B (pair A B a b) = b ;

you still get an error message:

DepType.gf:
DepType.gf:14:
Happened in the definition of function q
{a <> p A B (pair A B a b)}

It seems to me that for c = (pair A B a b),

El (B (p A B c)) = El (B (p A B (pair A B a b)))

is not the same as El (B a), so the computation rule for p apparently is
not available to prove

El (B (p A B (pair A B a b))) = El (B a).

I don't know why this is so.

Hans

[Shashank Pathak]

Oh thanks. Yes, I see the problem. Also, a small discussion on the GF discord resulted in the following PR (here) where normalisation is done during type checking