Названия запоминать я конечно не буду

нормальных - понятие растяжимое

есть containers, есть fgl

Ну, скажем, подходящих под задачу автора

Я просто с похожими целями смотрел

Просто по списку категорий (не тех) прошёлся с поиском и смотрел что есть

пока у меня смутное подозрени, что algebraic-graphs позволит граф "собрать", а fgl - "разобрать". Осталось найти третью либу, которая на лету сконвертит один граф в другой =)

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

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

https://hackage.haskell.org/package/type-level-sets-0.8.7.0/docs/Data-Type-Set.html

спасибо. в целом я думал, про тайп-левел сеты. но не был уверен, что все это можно увязать. а можно гдето почитать про ограничения type-level в хаскело-окамловых типов языков? что нельзя изобразить на тайплевеле , но можно в языке с полноценным завтипами?

пока у меня смутное подозрени, что algebraic-graphs позволит граф "собрать", а fgl - "разобрать". Осталось найти третью либу, которая на лету сконвертит один граф в другой =)

и контейнеры и фгл позволяют граф собирать, просто не так красиво как в случае с algebraic-graphs чтоб конвертировать вторые в первые надо или из интмапов которые умеет algebraic-graphs делать конвертировать или написать интерпретатор (инстанс класса Граф)

https://hackage.haskell.org/package/type-level-sets-0.8.7.0/docs/Data-Type-Set.html

это отличается от рекордов только сахаром?

спасибо. в целом я думал, про тайп-левел сеты. но не был уверен, что все это можно увязать. а можно гдето почитать про ограничения type-level в хаскело-окамловых типов языков? что нельзя изобразить на тайплевеле , но можно в языке с полноценным завтипами?

переход от значений к типам. то есть зависимые типы, собственно

ну, справедливости ради это уже и в хаскеле можно, только не шибко удобно

спасибо. в целом я думал, про тайп-левел сеты. но не был уверен, что все это можно увязать. а можно гдето почитать про ограничения type-level в хаскело-окамловых типов языков? что нельзя изобразить на тайплевеле , но можно в языке с полноценным завтипами?

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

это отличается от рекордов только сахаром?

поверх этой библиотеки сделана минимум одна рекордовая - буккипер

и контейнеры и фгл позволяют граф собирать, просто не так красиво как в случае с algebraic-graphs чтоб конвертировать вторые в первые надо или из интмапов которые умеет algebraic-graphs делать конвертировать или написать интерпретатор (инстанс класса Граф)

Спасибо. Я пошёл по второму пути =)

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

а есть может есть какаято статья в закладках, позволяющая подробней вникнуть в тайп-левел? или нужно штудировать тапл подробно и без этого никак (хотя там может этого и нету) ? Чтото читал , вроде понятно на простых примерах, но общей картины нету

а есть может есть какаято статья в закладках, позволяющая подробней вникнуть в тайп-левел? или нужно штудировать тапл подробно и без этого никак (хотя там может этого и нету) ? Чтото читал , вроде понятно на простых примерах, но общей картины нету

сейчас накидаю https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1009&context=compsci_pubs

спасибо. хм, кстати вижу в телеграме уже сохранено, видимо уже когдато от Вас сохранял на будущее) сейчас начну читать

а есть может есть какаято статья в закладках, позволяющая подробней вникнуть в тайп-левел? или нужно штудировать тапл подробно и без этого никак (хотя там может этого и нету) ? Чтото читал , вроде понятно на простых примерах, но общей картины нету

https://www.cs.ox.ac.uk/projects/utgp/school/andres.pdf

http://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf

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

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

спасибо! ну мне бы в целом "грокнуть" правильные паттерны мышления в подобных задачах кодирования

надо смотреть библиотеку https://github.com/goldfirere/singletons это передний край всего этого ужаса

да там нету правильных паттернов. есть "старая школа" тайплевел-пролога как тут http://www.cse.chalmers.se/~hallgren/Papers/hallgren.pdf

есть более современная, как в пейперах выше, она сейчас только формируется

ну и можно посмотреть видео докладов Richard A. Eisenberg и Stephanie Weirich

Какой же парсер у GHC нереальный

Что он делает для обработки ~ это просто тихий ужас

хорошо что не ленятся и используют один символ много для чего

Ну вообще ambiguity там нет, можно отличить, когда инфиксно, когда префиксно ~ используется

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

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

а инфиксным стал относительно недавно

Т.е. если написать a ~ b, это на самом деле App "a" (Lazy "b")

а инфиксным стал относительно недавно

Ну можно же по-человечески было делать его инфиксным

Вместо превращения App "a" (Lazy "b") в OpApp "a" "~" "b"

а в случае какого-нибудь ( ~a ?

Что это за случай с незакрытой скобкой?

ну она дельше закрывается, конечно

Кстати, да, вот собираются же мерджить type/term парсеры. Возьмем (~a). Это operator section или laziness annotation?

Да не просто собираются, а уже 2 недели 2 человека трудятся фултайм.

где человек = студент Эйзенберга

да так же как сейчас для велью парсера отличают a ! b от !b и b# c от b # c

тут-то ничего нового как раз

! whitespace sensitive что ли?

да

Дайте мне другой язык с нормальным синтаксисом

а как в нормальном будет?

GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Prelude> f !a = a Prelude> :info f <interactive>:1:1: error: Not in scope: ‘f’ Prelude> :info (!) (!) :: p1 -> p2 -> p2 -- Defined at <interactive>:1:3

ничего тут не отличается

А, надо -XBangPatterns включить

так банги не включены

все эти вайтспейс-сенситив штуки из-за синтаксиса, который добавили в расширениях

а как в нормальном будет?

вот так вот http://www.cse.chalmers.se/~nad/publications/danielsson-norell-mixfix.pdf

меджик хэш, лейблы, отрицательные литералы и т.д.

а еще "в нормальном" не будет отдельных неймспейсов для типов/тёрмов

и не придется писать '[a] вместо [a]

потому что [a] это List a

но это уродливо же, когда List a

а NonEmpty a ты как бы хотел писать?

[a]+ какой-нибудь небось

в нормальном языке не должно быть никакого NonEmpty

но вообще просто a+

a* тогда для списков?

ну да

Ну пусть так будет.

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

так что разные неймспейсы для них это фича

Юнит в идрисе тоже одинаковый

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

типы-то различаются у Foo :: a -> Foo a и Foo :: Type -> Type

но перегрузка это адище,

Ну типы и у [] различаются

я бы не стал связываться с таким

[] :: forall a. [a] vs [] :: Type -> Type

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

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

В нормальном языке ' быть не должно

это неприятно, но на такие жертвы можно пойти

Уж лучше List писать

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

т.е. на один ' тысячи List-ов будут

Прекрасный хаскель будущего

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

просто сейчас тайплевел совсем адище, его надо хоть в немного вменяемое состояние привести

пусть ради одной строки на тысячи нетайплевельных

да кому тёрм-левел нужен вообще

да кому тёрм-левел нужен вообще

TRIGGERED

[a]+ какой-нибудь небось

че за регексп)

ну надож перл сделать, куда без регекспов

Какое расширение даёт писать Type благословенный вместо б-гмерзкой *?

GHC 8

Not in scope: type constructor or class ‘Type’

{-# LANGUAGE DataKinds #-} import Data.Kind