type checking selections table (Ints n) [...] ! k

[Hans Leiss]

Hello Krasimir e.a.,

I have a question concerning type checking table selections like

table (Ints n) [value_0,...,value_n] ! k .

Apparently, it is never checked whether k =< n, but why? This has an
effect on possible linearization functions, see below.

It occurred to me in the following situation. While implementing some
missing functions of german/ConstructionGer.gf

Construction> gr -cat=Adv -tr -number=2 | l
timeHour twelveHour
um zwölf Uhr mittags

timeHour twentyTwoHour
um zehn Uhr abends

I thought that the Card argument in the function

-- timeHourMinute : Hour -> Card -> Adv ; -- at six forty a.m./p.m.
-- um sechs Uhr vierzig / um 6:40 Uhr
is too permissive, permitting for example

Lang> gr -number=2 -tr timeHourMinute threeHour ? | l
timeHourMinute threeHour (NumNumeral (num (pot2as3 (pot2plus pot01 pot110))))
um drei Uhr hundert &+ zehn nachts

timeHourMinute threeHour (AdNum (AdnCAdv less_CAdv) (NumDigits (IDig D_3)))
um drei Uhr weniger als 3 nachts

So my plan was to replace input type Card by a type Minute, defined via

oper
Min : PType = Predef.Ints 3 ; -- a parameter type by C.3.12 (short for 60)

lincat
Minute = { s : Str ; i : Min } ; -- a legal linearization type by C.3.8
-- even without s:Str

Then I wanted to generated |Min| many strings from auxiliary operations

oper
minutes : Min => Str = table {0 => "0" ; 1 => "1" ; 2 => "2" ; 3 => "3"} ;
minStr : {s:Str ; i:Min} -> Str = \mt -> minutes ! mt.i ; -- ignoring dummy s

and implement (say)

fun MinUtt : Minute -> Utt -- a legal fun declaration by C.3.4

by (say) using mkCard : Str -> Card composed with mkUtt : Card -> Utt:

lin MinUtt mt = -- a legal lin definition by C.3.9 (I think)
SyntaxGer.mkUtt (SyntaxGer.mkCard (minStr mt)) ;

But this causes an error:

Internal error in Compute.ConcreteNew:
Applying Predef.length: Expected a value of type String,
got VS (VV (App (Q (IC (Id {rawId2utf8 = "Predef"}),
IC (Id {rawId2utf8 = "Ints"}))) (EInt 3))
[VInt 0,VInt 1,VInt 2,VInt 3]
[VString "0",VString "1",VString "2",VString "3"])
(VP (VGen 0 []) (LIdent (Id {rawId2utf8 = "i"})))

As far as I see, thee problem comes from apparently unsufficient type
checks in the compiler. The oper minStr above, or the simpler

oper
min2Str : Min -> Str = \m -> minutes ! m ;

is not actually restricted to inputs of type Min:

> cc min2Str
\m -> table (Predef.Ints 3) ["0"; "1"; "2"; "3"] ! m

> cc minutes ! 4
table (Predef.Ints 3) ["0"; "1"; "2"; "3"] ! 4

> cc SyntaxGer.mkCard (minutes ! 4)
Internal error in Compute.ConcreteNew:
Applying Predef.length: Expected a value of type String,
got VS (VV (App (Q (IC (Id {rawId2utf8 = "Predef"}),
IC (Id {rawId2utf8 = "Ints"}))) (EInt 3))
[VInt 0,VInt 1,VInt 2,VInt 3]
[VString "0",VString "1",VString "2",VString "3"])
(VInt 4)

This is largely the compiler error generated from compiling the
linerazation function MinUtt above. However, in general the compiler
checks whether a selector argument is of the table input type:

> cc (table (ResGer.Case) ["0";"1";"2";"3"] ! 2)
type of 2
expected: ResGer.Case
inferred: Predef.Int

So, the question is why a corresponding check for table input types
(Ints n) is not made, and hence some (apparently legal) linearization
functions cannot be defined?

Best,
Hans

P.S. Maybe it isn't a really good idea to have a cat Minutes, which
would need 60 trees. Ignoring the dummy s in minStr is also not good.

Wiss.Mitarbeiter am CIS bis März 2017 (seitdem im Ruhestand)
-------------------------------------------------------------------------
Dr.Hans Leiß le...@cis.uni-muenchen.de
Centrum für Informations- www.cis.uni-muenchen.de/~leiss/
und Sprachverarbeitung (CIS)
Universität München
Oettingenstr. 67
D-80538 München
-------------------------------------------------------------------------