Test.gf

abstract Test = {

  cat
    NP ; S ;

  fun
    ANP, BNP, CNP : NP ;
    ConstNP : NP -> NP ;
    NP2S : NP -> S ; 
}

Test1ABC_makes_difference_Const_is_const.gf

concrete Test1ABC_makes_difference_Const_is_const of Test = open Prelude in {

  lincat
    NP = SS ** {abc : ABC} ;

  lin
    ANP = {s = "anp" ; abc = A} ;
    BNP = {s = "bnp" ; abc = B} ;
    CNP = {s = "cnp" ; abc = C} ;
    ConstNP np = np ** {abc = A} ; -- ConstNP is constant, it compiles to 1 concrete fun:  NP_* → NP_A
    NP2S np = {s =                 -- param ABC makes a difference in NP2S
      case np.abc of {
         A => np.s ++ "is an A" ;
         B => np.s ++ "is a B" ;
         C => np.s ++ "is a C"
       }
    } ;

  param
    ABC = A | B | C ;
}

{-
Concrete categories:
  S_0
  NP_1
  NP_2
  NP_3
  (_4 = coercion covering NP_1, NP_2, NP_3)
  
Concrete functions:
  ANP : NP_1
  BNP : NP_2
  CNP : NP_3
  ConstNP : _4 → NP_1
  NP2S : NP_1 → S_0
  NP2S : NP_2 → S_0
  NP2S : NP_3 → S_0
-}

Test2ABC_makes_difference_Const_isnt_const.gf

concrete Test2ABC_makes_difference_Const_isnt_const of Test = open Prelude in {

  lincat
    NP = SS ** {abc : ABC} ;

  lin
    ANP = {s = "anp" ; abc = A} ;
    BNP = {s = "bnp" ; abc = B} ;
    CNP = {s = "cnp" ; abc = C} ;
    ConstNP np = np ; -- ConstNP isn't actually constant
    NP2S np = {s =    -- param ABC makes a difference
      case np.abc of {
         A => np.s ++ "is an A" ;
         B => np.s ++ "is a B" ;
         C => np.s ++ "is a C"
       }
    } ;

  param
    ABC = A | B | C ;
}

{-
Concrete categories:
  S_0
  NP_1
  NP_2
  NP_3
  (no coercions)

Concrete functions:
  ANP : NP_1
  BNP : NP_2
  CNP : NP_3
  ConstNP : NP_1 → NP_1
  ConstNP : NP_2 → NP_2
  ConstNP : NP_3 → NP_3
  NP2S : NP_1 → S_0
  NP2S : NP_2 → S_0
  NP2S : NP_3 → S_0
-}

Test3ABC_doesnt_make_difference_Const_is_const.gf

concrete Test3ABC_doesnt_make_difference_Const_is_const of Test = open Prelude in {

  lincat
    NP = SS ** {abc : ABC} ;

  lin
    ANP = {s = "anp" ; abc = A} ;
    BNP = {s = "bnp" ; abc = B} ;
    CNP = {s = "cnp" ; abc = C} ;
    ConstNP np = np ** {abc = A} ; -- Const is const
    NP2S np = np ;                 -- param ABC makes no difference

  param
    ABC = A | B | C ;
}

{-
Concrete categories:
  S_0
  NP_1
  NP_2
  NP_3
  (_4 = coercion covering NP_1, NP_2, NP_3)
  
Concrete functions:
  ANP : NP_1
  BNP : NP_2
  CNP : NP_3
  ConstNP : _4 → NP_1
  NP2S : _4 → S_0
-}

Test4ABC_doesnt_make_difference_Const_isnt_const.gf

concrete Test4ABC_doesnt_make_difference_Const_isnt_const of Test = open Prelude in {

  lincat
    NP = SS ** {abc : ABC} ;

  lin
    ANP = {s = "anp" ; abc = A} ;
    BNP = {s = "bnp" ; abc = B} ;
    CNP = {s = "cnp" ; abc = C} ;
    ConstNP np = np ; -- Const isn't constant
    NP2S np = np ;    -- param ABC makes no difference

  param
    ABC = A | B | C ;
}

{-
Concrete categories:
  S_0
  NP_1
  NP_2
  NP_3
  (_4 = coercion covering NP_1, NP_2, NP_3)

Concrete functions:
  ANP : NP_1
  BNP : NP_2
  CNP : NP_3
  ConstNP : NP_1 → NP_1
  ConstNP : NP_2 → NP_2
  ConstNP : NP_3 → NP_3
  NP2S : _4 → S_0
-}