Приходится генерить из пурсы

purescript -> ts -> idris -> ts я ничего не упустил?))

эээ не так

Я решил в лоб сделать

idris -> ts

сначала хотел ts -> idris -> ts

пурса хз причем тут

когда генеришь херню

сначала хотел ts -> idris -> ts

но у идриса нет рантайм AST

или я не нашел)

я пока не тыкаю идрис) оставлю на весну

А че весной?

2.0?)

нет) просто не хочу напрягаться перед концом года)

А вообще у них там такая глубокая взаимосвязь всего подряд, что эффекты из ядра удалить нельзя

Путаешь вывод и следствие. Тип эффектов основан на row, но сам по себе row (#) ничего ге знает про эффекты и выпилить эффекты, оставив # не проблема

Не эффекты же удаляют

А row

Из типа

У нас все иммутабельно, когда берут тип и выбрасывают из него один параметр, они создают новый тип)

было log :: forall e. Eff ( console :: CONSOLE ) e станет log :: forall e. IO e

У нас все иммутабельно, когда берут тип и выбрасывают из него один параметр, они создают новый тип)

ну оке

Не, там фишка именно в том, что e внутри тайплевел множества

было log :: forall e. Eff ( console :: CONSOLE ) e станет log :: forall e. IO e

а как record вид накручивать эффекты?

log :: String -> forall e. Eff (console :: CONSOLE | e) Unit => log :: String -> IO Unit

Eff (console :: CONSOLE, db:: DB | e) а ща надо трансформеры накручивать будет?

Это же пурса, тут расширяемые эффекты сильно упрощены, это не фрир.

ДБ тут означает лишь то, что код вызывает что-то в жс, теперь это тоже будет ИО

Стеки трансформеров для локальных эффектов как были раньше, так и остаются

кривая пурса)

Ну вот они переименовали Ефф в ио и освободили имя, может появится фрир теперь какой, благо роу полиморфизм есть, писать всякие IsElem констрейты не нужно

где-то был)

https://github.com/natefaubion/purescript-run

А, да, точно

У меня такое чувство, будто Фил пожертвовал тайплами из-за роу-полиморфизма

было log :: forall e. Eff ( console :: CONSOLE ) e станет log :: forall e. IO e

а что за CONSOLE

CONSOLE :: Effect (каинд)

Это просто метка фантомная

ооооо

https://github.com/purescript/purescript-console/blob/master/src/Control/Monad/Eff/Console.purs#L10

https://github.com/purescript/purescript-console/blob/master/src/Control/Monad/Eff/Console.purs#L10

ну это не фантом

В пурсе это таки фантом, он используется чисто для того, чтобы показать коду ниже, что там есть вызов в жс-ные функции этого модуля

Eff в пурсе - это IO + тайплевел множество из фантомных меток. Как я понял, оно очень быстро росло и поэтому это тайплевел множество убрали из типа

вводило в оману хаскелл разрабов)

У меня такое чувство, будто Фил пожертвовал тайплами из-за роу-полиморфизма

Тайпл?

Тупл) кортеж

А что с таплами в пурсе?

А их нет в прелюдии

Можно самому опредклить как data Tuple a b = Tuple a b Есть либа внешняя с точно таким же определением

ну есть смешной конструктор /\ привет тебе логика (конъюнкция)

кстати как вы различаете что есть \/ и что есть /\? я для себя придумал прикольный признак

кстати как вы различаете что есть \/ и что есть /\? я для себя придумал прикольный признак

(a,b) vs Either a b?

ну в типах да, а я про логику (логические операторы)

/\ похоже на возведение в степень (или стрелку Кнута), а умножение и конъюнкция схожи

у меня было проще)) если спустить 2 шарика по сторонам /\ то оба дойдут конца (и), а если шарики катнуть как-то так \/ то только один дойдет (или)

кстати как вы различаете что есть \/ и что есть /\? я для себя придумал прикольный признак

за 3 курса универа разной логики как-то запомнилось

выглядело грубо :(

?

Че за хуйня

Почему у меня в универе только с89

?

я электронщик, нам нужно было)

Аа, ясно

имо оно всем программистам нужно

имо оно всем программистам нужно

ой не, 3 курса говном занимались, все можно было в два семестра уместить

ERROR: S client not available

ну это да

Кто-нибудь пуллреквестните клиент телеграма без кнопки удаления своих сообщений

Мне запомнилось тем что \/ чаще видишь, значит другую операцию подобно умножению просто опускают при письме. Ну и умножение легко ассоциировать На самом деле эти операторы нифига не интуитивные и за многие семестры никак не запоминались

а как их вообще выбрали?

а как их вообще выбрали?

От объединения и пересечения множеств

ну а там

По-моему на латыни тоже это называется как Union

ну да, это ж еще из школьной геометрии например

ой не, 3 курса говном занимались, все можно было в два семестра уместить

2 курса говном занимаемся 4 курс говорит, что ничего не изменилось

2 курса говном занимаемся 4 курс говорит, что ничего не изменилось

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

а как в различных логиках интерпретируют вероятные события?

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

напр "возможно ч.л. произойдет"

Как то само собой запомнилось

это же всегда правда?

ну в твоих высказываниях в логику добавляется ось времени где события имеют некоторый порядок друг относительно друга

ооо

и как бы есть лтр

что за лтр?

но оно не про вероятности, хотя такие как у тебя высказывания вроде можно выразить

Го нечёткую логику сразу

Там оно всё и выразится

линейно-темпоральная логика (не путать с линейной логикой и темпоральной логикой)

линейная это классическая?

напр "возможно ч.л. произойдет"

Чем отличается тогда кванта всеобщности от кванты существования

из интересных штук которые ей пользуются: spin и promela, dejafu и далее

Почитай книгу по базовой формальной логике

линейно-темпоральная логика (не путать с линейной логикой и темпоральной логикой)

И это

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

Жиза

линейная это классическая?

вовсе нет относительно хайповая тема, особенно в этих важих растах