13/9/2011 by AR

Main files

  Types.gf     -- Martin-Löf's "Intuitionistic Type Theory" (book 1984)
  TypesSymb.gf -- concrete syntax close to the notation of the book

Experimental extension

  Donkey.gf    -- sentences about men and donkeys, with Montague semantics in Types
  DonkeyEng.gf -- quick and dirty English concrete syntax

Example 1: the formula for the "donkey sentence", 
"if a number is equal to a number, it is equal to it"
The parser restores implicit arguments, and linearizing the formula back returns it with
Greek letters (which could also be used in the input):
 
  > import TypesSymb.gf

  Types> p -tr -cat=Set "( Pi z : ( Sigma x : N ) ( Sigma y : N ) I ( N , x , y ) ) I ( N , p ( z ) , p ( q ( z ) ) )" | l -unlexcode

  Pi 
    (Sigma Nat (\x -> 
      Sigma Nat (\y -> Id Nat x y))) 
    (\z -> 
      Id Nat 
        (p {Nat} {\_1 -> Sigma Nat (\v2 -> Id Nat _1 v2)} 
           z) 
        (p {Nat} {\_1 -> Id Nat (p Nat (\v2 -> Sigma Nat (\v3 -> Id Nat v2 v3)) z) _1} (
           q {Nat} {\_1 -> Sigma Nat (\v2 -> Id Nat _1 v2)} 
             z)))

  (Π z : (Σ x : N)(Σ y : N)I (N , x , y))I (N , p (z), p (q (z)))


Example 2: parse and interpret a sentence, also showing the nice formula.

  > import DonkeyEng.gf

  Donkey> p -cat=S -tr "a man owns a donkey " | pt -transfer=iS -tr | l -unlexcode

  PredVP {Man'} (An Man) (ComplV2 {Man'} {Donkey'} Own (An Donkey))

  Sigma Man' (\v0 -> Sigma Donkey' (\v1 -> Own' v0 v1))

  (Σ v0 : man')(Σ v1 : donkey')own' (v0 , v1)


Example 3: (to be revisited) parse of "the donkey sentence" fails, but should succeed

  Donkey> p -cat=S "if a man owns a donkey he beats it"

  The sentence is not complete
 
  Donkey> p -cat=S "if a man owns a donkey the man beats the donkey"

  The sentence is not complete


Example 4: problem that appears with CN's modified by polymorphic AP's (old), but not with monomorphic ones (pregnant)

  Donkey> p "an old man walks"
  src/runtime/haskell/PGF/TypeCheck.hs:(528,4)-(550,67): Non-exhaustive patterns in function occurCheck
  -- this should build (ModCN Man (Old Man'))

  Donkey> p "a pregnant woman loves John " | pt -transfer=iS | l -unlexcode
  (Σ v0 : (Σ v0 : woman')pregnant' (v0))love' (v0 , john')
