# Dependent Type Theory in Abstract Syntax

22 views

### Shashank Pathak

Oct 1, 2023, 1:44:26 AM10/1/23
to Grammatical Framework
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

Oct 6, 2023, 3:06:54 PM10/6/23
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