Здравейте. Имам въпрос върху следните записки:
......
reads*((E=>i)=>i)=>E (a(book))(E=>i)=>i
reads*(a(book))((E=>i)=>i)=>i
....
Притесняват ме типовете и по-точно reads* приема (E=>i)=>i) и връща E. Имаме (a(book))(E=>i)=>i. Защо резултатът не е от тип Е и как сме получили типа на резултата?
Най-вероятно съм допуснал техническа грешка като съм писал на дъската. Би трябвало типът на reads* да е ((ε ⇒ ι) ⇒ ι) ⇒ ((ε ⇒ ι) ⇒ ι) ⇒ ι. Така типовете вече са правилни.
Защо е така? Понеже стандартният тип на reads (транзитивен глагол) е ε ⇒ ε ⇒ ι (което се тълкува като "ако ми дадеш обект и още един обект ще ти построя информативно изречение"). В случая reads* е получен като е приложено "повдигане на типовете" над двата аргумента ε, като повдигането се състои в замяната на ε с (ε ⇒ ι) ⇒ ι.
