D
плюсы и хаскель
Size: a a a
2021 April 02
D
ядреная смесь
AG
то есть система неидемпотентных типов пересечений это по факту индексированное АСТ, где в узлах для применения вшито сколько раз будет использоваться функция
AG
в общем то ничего неожиданного, но забавно видеть, как завтипы заставляют протаскивать именно эту инфу
AG
фактически как и показал де карвальо, это та же линейная система типов, но (суб)экспоненциалы как бы вклеены в типы
AG
ex1 : TermT [] Test1 ([[V] ~> V] ~> [V] ~> V)
ex1 = LamT $ LamT $ App1 {ns1=[0,1]} {ns2=[1,0]}
(VarT $ Suc Zero)
(VarT Zero)
ex2 : TermT [] Test2 ([[V] ~> V, [V] ~> V] ~> [V] ~> V)
ex2 = LamT $ LamT $ App1 {ns1=[0,1]} {ns2=[1,1]}
(VarT $ Suc Zero) $
App1 {ns1=[0,1]} {ns2=[1,0]}
(VarT $ Suc Zero)
(VarT Zero)
w
ex1 : TermT [] Test1 ([[V] ~> V] ~> [V] ~> V)
ex1 = LamT $ LamT $ App1 {ns1=[0,1]} {ns2=[1,0]}
(VarT $ Suc Zero)
(VarT Zero)
ex2 : TermT [] Test2 ([[V] ~> V, [V] ~> V] ~> [V] ~> V)
ex2 = LamT $ LamT $ App1 {ns1=[0,1]} {ns2=[1,1]}
(VarT $ Suc Zero) $
App1 {ns1=[0,1]} {ns2=[1,0]}
(VarT $ Suc Zero)
(VarT Zero)
а можно рисунок фотографии скриншота?
AT
а можно рисунок фотографии скриншота?
Да
AG
ну и там дальше так же типизируется машина кривина (применения размазываются между замыканиями и стеком), и можно протащить через эти типы пруф о том что количество шагов машины равно размеру терма
R
ex1 : TermT [] Test1 ([[V] ~> V] ~> [V] ~> V)
ex1 = LamT $ LamT $ App1 {ns1=[0,1]} {ns2=[1,0]}
(VarT $ Suc Zero)
(VarT Zero)
ex2 : TermT [] Test2 ([[V] ~> V, [V] ~> V] ~> [V] ~> V)
ex2 = LamT $ LamT $ App1 {ns1=[0,1]} {ns2=[1,1]}
(VarT $ Suc Zero) $
App1 {ns1=[0,1]} {ns2=[1,0]}
(VarT $ Suc Zero)
(VarT Zero)
каждый раз я ловлю вайбы лиспа
AG
ну это просто
λf.λx.f x и λf.λx.f (f x)AG
только тип заставляет указывать количество использований
AG
а рантаймовый коррелят типа это список длин кодоменов
AG
у эрхарда есть аналогичная штука для CBV, можно попробовать аналогичный пруф для CEK
AG
или может забить и копать дальше соответствия с HO/N-играми
P
или может забить и копать дальше соответствия с HO/N-играми
SK
то есть как релиз в апреле
AG
семья наелась пельменей и заснула :)