ΑZ
но вообще затем же зачем в графах разделяют ребра и узлы
Size: a a a
2021 May 26
ΑZ
прост так удобно, такое определение
AN
так а что это за книжка была
TK
Ещё бы знать, что такое термы
B
так такие пруфы строить ессесна
AN
выше же определение о_О
TK
Дяди-то умные, но понимаю только колхозно
ΑZ
Type_theory_and_formal_proof Nederpelt
ΑZ
нет, такие пруфы норм
ΑZ
у меня есть стейтмашина в компайл тайм
ΑZ
data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
NewGame : (word : String) -> GameCmd () NotRunning (const (Running 6 (length (letters word))))
Won : GameCmd () (Running (S guesses) 0) (const NotRunning)
Lost : GameCmd () (Running 0 (S guesses)) (const NotRunning)
Guess : (c : Char) -> GameCmd GuessResult (Running (S guesses) (S letters))
(
\res => case res of
Correct => Running (S guesses) letters
Incorrect => Running guesses (S letters)
)
ShowState : GameCmd () state (const state)
Message : String -> GameCmd () state (const state)
ReadGuess : GameCmd Char state (const state)
Pure : (res : ty) -> GameCmd ty (state_fn res) state_fn
(>>=) : GameCmd a state1 state2_fn -> ((res : a) -> GameCmd b (state2_fn res) state3_fn) -> GameCmd b state1 state3_fnΑZ
зацените матч в типах
ΑZ
или то что
GameCmd имеет типGameCmd<t:T, S, Fn(t -> S)>AN
о там есть глава types dependent on types
AN
и types dependent on terms
ΑZ
типы зависимые от типов это обычные генерики
ΑZ
а второе это уже полноценные завтипы, да
TK
Не люблю теоремы. Начал вчитываться, там определяют не термы, а лямбда-термы, откуда-то берут M и N (Множества? Подмножества? Семейства? Алфавиты? Что это?), не объясняют, что из себя переменные представляют, берут и делают тупл, который как-то ни к селу, ни к городу. Обмазали всё локальными нотациями, пойди и пойми их потом.
ΑZ
ну там это типа 50ая страница, часть определений даны выше, часть ты уже должен знать (типа что такое множество)
AN
то не теорема. Кек