b
конечно можно составить пропозицию, которую можно трактовать по–разному
Size: a a a
2020 October 16
b
в таком случае парсер попросит тебя расставить скобки
b
но на практике такое встречается не слишком часто
EG
id := iota.
id x :=
x := iota.
-> iota.
x id y :=
x, y := iota.
-> iota.
EG
id := iota.
id x :=
x := iota.
-> iota.
x id y :=
x, y := iota.
-> iota.
id id id — это что?b
id := iota.
id x :=
x := iota.
-> iota.
x id y :=
x, y := iota.
-> iota.
что значит
-> iota.?EG
что значит
-> iota.?«Если x — йота, то id x — тоже йота»
b
id x это пропозиция, а не знакEG
Или давай сделаем типа unit type.
unit_t := iota.Соответственно,
unit := unit_t.
f := unit_t.
f x :=
x := unit_t.
-> unit.
x f y :=
x, y := unit_t.
-> unit.
f f f непонятно, как распарситьEG
Совсем непонятно, как это сделать эффективно
EG
У тебя у самого есть работающий пример?
b
опять что значит
f x -> unit.b
ну типа ты делаешь бестолковые пропозиции
EG
опять что значит
f x -> unit.«Если в выражении
f x x имеет тип unit_t, то значение выражения — unit»b
возвращаешь то iota, то unit
b
это бестолковые знаки, ты ничего с ними не сделаешь
b
что значит “значение выражения unit”?
b
в логосе это значит что ты буквально вместо этой пропозиции можешь подставить знак
unitEG
f x это юнит если x — unitb
я если честно не понимаю зачем это вообще может быть нужно