Grammatical Framework: "linearization type field cannot be Int"; how to write a concrete syntax for grammar with arithmetic expressions?

Question

I'm trying to write a concrete syntax for this grammar (from Chapter 6 in Grammatical Framework: Programming with Multilingual Grammars):

abstract Arithm = {
  flags startcat = Prop ;
  cat
    Prop ;                        -- proposition
    Nat ;                         -- natural number
  fun
    Zero : Nat ;                  -- 0
    Succ : Nat -> Nat ;           -- the successor of x
    Even : Nat -> Prop ;          -- x is even
    And  : Prop -> Prop -> Prop ; -- A and B
}

There are predefined categories for integer, float and string literals (Int, Float and String), and they can be used as arguments to functions, but they may not be value types of any function.

In addition, they may not be used as a field in a linearisation type. This is what I would like to do, using plus defined in Predef.gf:

concrete ArithmEng of Arithm =
  open Predef, SymbolicEng, SyntaxEng, ParadigmsEng in
  lincat
    Prop = S ;
    Nat  = {s : NP ; n : Int} ;
  lin
    Zero     = mkNat 0 ;
    Succ nat = let n' : Int = Predef.plus nat.n 1 in mkNat n' ;
    Even nat = mkS (mkCl nat.s (mkA "even")) ;
    And p q  = mkS and_Conj p q ;
  oper
    mkNat  : Int -> Nat ;
    mkNat int = lin Nat {s = symb int ; n = int} ;
} ;

But of course, this does not work: I get the error "linearization type field cannot be Int".

Maybe the right answer to my question is to use another programming language, but I am curious, because this example is left as an exercise to the reader in the GF book, so I would expect it to be solvable.

I can write a unary solution, using the category Digits from Numeral.gf:

concrete ArithmEng of Arithm =
  open SyntaxEng, ParadigmsEng, NumeralEng, SymbolicEng, Prelude in {
  lincat
    Prop = S ;
    Nat = {s : NP ; d : Digits ; isZero : Bool} ;
  lin
    Zero = {s = mkNP (mkN "zero") ; d = IDig D_0 ; isZero = True} ;
    Succ nat = case nat.isZero of {
                 True  => mkNat (IDig D_1) ;
                 False => mkNat (IIDig D_1 nat.d) } ;
    Even nat = mkS (mkCl nat.s (mkA "even")) ;
    And p q  = mkS and_Conj p q ;
  oper
    mkNat : Digits -> Nat ;
    mkNat digs = lin Nat {s = symb (mkN "number") digs ; d = digs ; isZero = False} ;
} ;

This produces the following results:

Arithm> l -bind Even Zero
zero is even

0 msec
Arithm> l -bind Even (Succ Zero)
number 1 is even

0 msec
Arithm> l -bind Even (Succ (Succ (Succ Zero)))
number 111 is even

This is of course a possible answer, but I suspect this is not the way the exercise was intended to be solved. So I wonder if I'm missing something, or if the GF language used to support more operations on Ints?

Ias

Answer 1

A possible, but still rather unsatisfactory answer, is to use the parameter Ints n for any natural number n.

Notice the difference:

• Int is a literal type, just like String and Float.
• All literals have {s : Str} as their lincat in every concrete syntax, and you can't change it in any way.
• Since the lincat contains Str (not String), you are not allowed to pattern match it at runtime.

Introducing Ints n: a parameter type

However, Ints n is a parameter type, because it's finite. You may have seen Ints n in old RGL languages, like the following Finnish grammar:

-- from the Finnish resource grammar
oper
  NForms : Type = Predef.Ints 10 => Str ;

  nForms10 : (x1,_,_,_,_,_,_,_,_,x10 : Str) -> NForms =
    \ukko,ukon,ukkoa,ukkona,ukkoon,
       ukkojen,ukkoja,ukkoina,ukoissa,ukkoihin -> table {
    0 => ukko ;   1 => ukon ;    2 => ukkoa ;
    3 => ukkona ; 4 => ukkoon ;  5 => ukkojen ;
    6 => ukkoja ; 7 => ukkoina ; 8 => ukoissa ;
    9 => ukkoihin ; 10 => ukko
    } ;

What's happening here? This is an inflection table, where the left-hand side is… just numbers, instead of combinations of case and number. (For instance, 5 corresponds to plural genitive. Yes, it is completely unreadable for anyone who didn't write that grammar.)

That same code could as well be written like this:

-- another way to write the example from the Finnish RG
param
  NForm = SgNom | SgGen | … | PlGen | PlIll ; -- Named params instead of Ints 10
oper
  NForms : Type = NForm => Str ;

  nForms10 : (x1,_,_,_,_,_,_,_,_,x10 : Str) -> NForms =
    \ukko,ukon,ukkoa,ukkona,ukkoon,
       ukkojen,ukkoja,ukkoina,ukoissa,ukkoihin -> table {
    SgNom => ukko ; 
    SgGen => ukon ;
    ...
    PlGen => ukkojen ;
    PlIll => ukkoihin
    } ;

As you can see, the integer works as a left-hand side of a list: 5 => ukkojen is as valid GF as PlGen => ukkojen. In that particular case, 5 has the type Ints 10.

Anyway, that code was just to show you what Ints n is and how it's used in other grammars than mine, which I'll soon paste here.

Step 1: incrementing the Ints

Initially, I wanted to use Int as a field in my lincat for Nat. But now I will use Ints 100 instead. I linearise Zero as {n = 0}.

concrete ArithmC of Arithm = open Predef in {
  lincat
    Nat = {n : Ints 100} ;
  lin
    Zero = {n = 0} ; -- the 0 is of type Ints 100, not Int!

Now we linearise also Succ. And here's the exciting news: we can use Predef.plus on a runtime value, because the runtime value is no longer on Int, but Ints n---which is finite! So we can do this:

  lin
    Succ x = {n = myPlus1 ! x.n} ;

  oper
    -- We use Predef.plus on Ints 100, not Int
    myPlus1 : Ints 100 => Ints 100 = table {
      100 => 100 ;           -- Without this line, we get error
      n => Predef.plus n 1   -- magic!
      } ;
}

As you can see from myPlus1, it's definitely possible to pattern match Ints n at runtime. And we can even use the Predef.plus on it, except that we must cap it at the highest value. Without the line 100 => 100, we get the following error:

- compiling ArithmC.gf... Internal error in GeneratePMCFG:
    convertTbl: missing value 101
                among 0
                      1
                      ...
                      100

Unfortunately, it's restricted to a finite n.

Let's test this in the GF shell:

$ gf
…

> i -retain ArithmC.gf 

> cc Zero
{n = 0; lock_Nat = <>}

> cc Succ Zero
{n = 1; lock_Nat = <>}

> cc Succ (Succ (Succ (Succ (Succ Zero))))
{n = 5; lock_Nat = <>}

Technically works, if you can say that. But we can't do anything interesting with it yet.

Step 2: Turn the Ints n into a NP

Previously, we just checked the values in a GF shell with cc (compute_concrete). But the whole task for the grammar was to produce sentences like "2 is even".

The lincat for Int (and all literal types) is {s : Str}. To make a literal into a NP, you can just use the Symbolic module.

But we cannot increment an Int at runtime, so we chose to use Ints 100 instead.

But there is no lincat for Ints n, because it's a param. So the only way I found is to manually define a showNat oper for Ints 100.

This is ugly, but technically it works.

concrete ArithmEng of Arithm =
  open Predef, SymbolicEng, SyntaxEng, ParadigmsEng in {
  lincat
    Prop = S ;
    Nat  = {s : NP ; n : MyInts} ;
  oper
    MyInts = Ints 100 ;
  lin
    Zero     = mkNat 0 ;
    Succ nat = mkNat (myPlus1 ! nat.n) ;
    Even nat = mkS (mkCl nat.s (mkA "even")) ;
    And p q  = mkS and_Conj p q ;
  oper
    mkNat : MyInts -> Nat ;
    mkNat i = lin Nat {s = symb (showNat ! i) ; n = i} ;

    myPlus1 : MyInts => MyInts = table {
      100 => 100 ;
      n => Predef.plus n 1
      } ;

    showNat : MyInts => Str ;
    showNat = table {
      0 => "0" ; 1 => "1" ; 2 => "2" ;
      3 => "3" ; 4 => "4" ; 5 => "5" ;
      6 => "6" ; 7 => "7" ; 8 => "8" ;
      9 => "9" ; 10 => "10" ; 11 => "11" ;
      12 => "12" ; 13 => "13" ; 14 => "14" ;
      15 => "15" ; 16 => "16" ; 17 => "17" ;
      18 => "18" ; 19 => "19" ; 20 => "20" ;
      _ => "Too big number, I can't be bothered"
      } ;
} ;

Let's test in the GF shell:

Arithm> gr | l -treebank
Arithm: Even (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))
ArithmEng: 12 is even

So yes, technically it works, but it's unsatisfactory. It only works for a finite n, and I had to type out a bunch of boilerplate in the showNat oper. I'm still unsure if this was the intended way by the GF book, or if GF used to support more operations on Int.

Other solutions

Here's a solution by daherb, where Zero outputs the string "0" and Succ outputs the string "+1", and the final output is evaluated in an external programming language.

Ias