Телеграмм чат группы haskellru страница 14378

13:52пожаловаться #1

2020 October 28

K

А кто скажет, что погуглить-почитать по сессионным типам, чтобы вот такую штуку сделать.

Хочется генерить dual сессионные типы к исходному типу (клиенткиий протокол генерить по северному и наоборот). При этому генерить в рантайме, но прочекать генератор в компайл тайм? Я многого хочу и тут уже dependent types нужны? (Сам серверный протокол будет мутировать, поэтому нужно генерить клиентскую часть)

11:38пожаловаться #2

KV

KLH

А кто скажет, что погуглить-почитать по сессионным типам, чтобы вот такую штуку сделать.

Хочется генерить dual сессионные типы к исходному типу (клиенткиий протокол генерить по северному и наоборот). При этому генерить в рантайме, но прочекать генератор в компайл тайм? Я многого хочу и тут уже dependent types нужны? (Сам серверный протокол будет мутировать, поэтому нужно генерить клиентскую часть)

Протокол мутирует в рантайме?

11:48пожаловаться #3

AV

Для "проверки" протокола мутирующего в рантайме нужны зависимые типы

11:51пожаловаться #4

KV

И то если он мутирует по каким-то проверяемым правилам, а не произвольно

11:51пожаловаться #5

AV

Если не мутирует, то не факт, что и сессионные типы нужны, они вообще нужны чтобы тайпчекать, что код соотвествет протоколу

11:51пожаловаться #6

AV

Типа, вызываются методы, которые разрешены в этом состоянии, что тоже можно без сессионных типов, конечно, но чуть печальнее

11:52пожаловаться #7

KV

Непонятно, мутирующий протокол — это просто тип, который меняется от вызовов (тогда просто индексированные монады можно использовать), или же этот меняющийся тип сам по себе ещё может меняться

11:54пожаловаться #8

KV

Теоретически, можно представить клиент и сервер как индексированные свободную монаду и косвободную комонаду с пейрингом, и тогда можно одно сгенерировать по другому, неважно в какую сторону. Но это жесть

11:55пожаловаться #9

KV

А если ещё и протокол меняется, то точно типы не помогут

11:56пожаловаться #10

K

Kirill Valyavin

Протокол мутирует в рантайме?

Да, меняется в рантайме. И да, понимаю, что наверное просто сесионными типами не отделаешься

11:59пожаловаться #11

KV

Well-Typed Communication Protocols | SkillsCast

Вообще ИРЛ делют как-то так, но там ничё не меняется в рантайме
https://skillsmatter.com/skillscasts/14633-45-minute-talk-by-duncan-coutts

Haskell eXchange 2019 conference cast. Duncan Coutts: Concurrency is still hard. Building distributed applications using message passing is still hard. Appli...

12:00пожаловаться #12

K

Клиент и сервер могут быть некоторыми интерпретаторами. И хотелось бы строить некий ast для них непротиворечивый и менять его непротиворечиво в рантайме. Тут gadt может пригодится наверное

12:00пожаловаться #13

K

Well-Typed Communication Protocols | SkillsCast

Kirill Valyavin

Вообще ИРЛ делют как-то так, но там ничё не меняется в рантайме
https://skillsmatter.com/skillscasts/14633-45-minute-talk-by-duncan-coutts

Haskell eXchange 2019 conference cast. Duncan Coutts: Concurrency is still hard. Building distributed applications using message passing is still hard. Appli...

Спасибо, чекну

12:00пожаловаться #14

KV

KLH

Клиент и сервер могут быть некоторыми интерпретаторами. И хотелось бы строить некий ast для них непротиворечивый и менять его непротиворечиво в рантайме. Тут gadt может пригодится наверное

А как оно меняется в рантайме вообще? С примером проще будет

12:02пожаловаться #15

AV

Это про STM доклад?

12:02пожаловаться #16

KV

Alexander Vershilov

Это про STM доклад?

Нет

12:02пожаловаться #17

AV

Ок!

12:03пожаловаться #18

K

Kirill Valyavin

А как оно меняется в рантайме вообще? С примером проще будет

Грубо говоря, tcp сервер и клиент на полностью своем стеке. И вот нужно немного "взаимно нарушать" принятые правила tcp-ip-"общения")

12:05пожаловаться #19

KV

KLH

Грубо говоря, tcp сервер и клиент на полностью своем стеке. И вот нужно немного "взаимно нарушать" принятые правила tcp-ip-"общения")

Ничё не понятно. Но в общем если у Вас просто стейт-машина на уровне типов, где при каждом текущем стейте определён набор доступных вызовов, то это просто сессионные типы, а если эта стейт-машина ещё и меняется в зависимости от рантайм-значений, то это сессионные + зависимые типы, ну и есть шанс, что хаскеля хватит для этого