22 views

Skip to first unread message

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 ;

}

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.

Oct 6, 2023, 3:06:54 PM10/6/23

to gf-...@googlegroups.com, gf-...@googlegroups.com

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 ;

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

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

Oct 13, 2023, 7:09:03 AM10/13/23

to Grammatical Framework

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu