SP
ну я хотел бы посмотреть
Size: a a a
2020 February 13
SP
там есть какой то рантайм шелл?
λ
Рантайм шелл? Как для жса консоль в браузере?
λ
Не, такого нету конечно
SP
Рантайм шелл? Как для жса консоль в браузере?
да
SP
ну без такого я не понимаю как некоторые вещи делать
SP
вернее понимаю частично. миша говорил что делается тест и на тексте сразу кнопка, но чето хз
EG
правда что за операторы :*: :~: я не знаю
Также Алекс: операторы в Хаскелле понятные и логичные.
λ
кто шарит в typelevel equality? как такую елку победить?
mulComm :: Natural m -> Natural n -> m :*: n :~: n :*: m
mulComm NumZ NumZ = T.Refl
mulComm (NumS pm) NumZ = case mulComm pm NumZ of T.Refl -> T.Refl
mulComm NumZ (NumS pn) = case mulComm NumZ pn of T.Refl -> T.Refl
mulComm (NumS m) (NumS n) =
case mulComm m (NumS n) of
T.Refl -> case mulComm n (NumS m) of
T.Refl -> case addAssoc n m (mulP n m) of
T.Refl -> case addAssoc m n (mulP m n) of
T.Refl -> case addComm m n of
T.Refl -> case mulComm m n of T.Refl -> T.Refl
Тут кейс выполняет функцию рерайта из идриса (на самом деле рерайт в идрисе это сахар для кейса)
λ
правда что за операторы :*: :~: я не знаю
Это тайплевел умножение и тайплевел эквалити
λ
Про тайплевел умножение это просто предположение, но скорее всего так и есть
EG
Это тайплевел умножение и тайплевел эквалити
В чем-то логично, могу согласиться
EG
Типа :: и *
EG
Но угадать это нереально
λ
Типа :: и *
Тут другая логика, инфиксные конструкторы типов в хаскеле должны начинаться на двоеточие
SP
я тут поигрался кстати с монадками. такое дело - никак не узнать что код не требует ио. т.е. такой тупой я предполагаю что ио это такой СЕРВИС. в тс если у меня сервис не юзается - я вижу, и могу сказать мол окей, сервис мне тут больше не нужен. в хаскеле же я имею функцию IO () которая просто делает return 1 и я как бы вынужден использовать ио. или я должен просто увидеть типа ой мне тут не нужен ретурн или просто убрать ио и попытаться все сделать без него, но тоже чето не вяжется
EG
Тут другая логика, инфиксные конструкторы типов в хаскеле должны начинаться на двоеточие
Ну, второе двоеточие там быть не обязано
EG
я тут поигрался кстати с монадками. такое дело - никак не узнать что код не требует ио. т.е. такой тупой я предполагаю что ио это такой СЕРВИС. в тс если у меня сервис не юзается - я вижу, и могу сказать мол окей, сервис мне тут больше не нужен. в хаскеле же я имею функцию IO () которая просто делает return 1 и я как бы вынужден использовать ио. или я должен просто увидеть типа ой мне тут не нужен ретурн или просто убрать ио и попытаться все сделать без него, но тоже чето не вяжется
Ась?
λ
Вот и оборачивают обычно вэльюлевел операторы в два двоеточия
λ
Ну, второе двоеточие там быть не обязано
Для симметрии обычно делают 2