знайте это и бойтесь нас

я однажды написал возведение в степень для чисел Чёрча в Coq, но до сих пор не понимаю как это работает.

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

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

при этом ты всё-таки решил задачу. вот как это работает?

человеческий мозг работает по странным механизмам

это вообще не компьютер

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

это какая-то машина для нечеткого паттерн-матчинга

в spacemacs кстати завезли coq layer (просто proof general прикрутили)

я опробовал, всё ок

можете теперь пользоваться

Его же вроде дропнули

уже?

но зачем

(((

А, для coq может нет

Но вот для isabelle точно отказались

В пользу штуки на базе jedit

а почему?

хмм

кстати

а есть профит использовать intero вместо ghci не в ide, а в качестве обычного repl?

я вот так и не понял

и вообще что в хаскеле с альтернативными ghci?

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

(просто в других языках появляются альтернативные repl)

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

у тебя в универе это было? или онлайн курс? или просто как я самостоятельно Software Foundations проходишь?

там вроде кроме подсветки ничего и не придумать

ну разве что мб haskellDo но это не консолька

В атоме в хаскельном наборе плагинов есть repl. Его особенность в том, что можно писать многострочные выражения. И ошибки пишет не в repl, а в отдельную панель с ошибками.

В атоме в хаскельном наборе плагинов есть repl. Его особенность в том, что можно писать многострочные выражения. И ошибки пишет не в repl, а в отдельную панель с ошибками.

А в ghci тоже можно, :set +m

Ну да. Сложно придумать особо инновационное что-то. Разве что ноутбуки типа jupyter ihaskell haskelldo...

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

Я слышал что stack работает на форке, но не уверен так ли это и что они туда добавили со своей стороны не знаю

нет конечно

обычный ghci там

Я слышал что stack работает на форке, но не уверен так ли это и что они туда добавили со своей стороны не знаю

А... или я перепутал и это не stack, а intero для emacs что-то там форкнул

в интеро уже возможно ghc API явно используется

Вот, точно https://commercialhaskell.github.io/intero/ The Intero backend used by the Emacs mode is a fork of GHCi, it behaves like your old friend GHCi, but with more features.

но ghci завязано на ghc сильно, так что если морда другая а внутренности те же. другой интерпретатор это hugs

надо посмотреть насколько там форк

https://repl.it/site/blog/haskell

Это прекрасно

А вот какие у нас есть приемы для расширяемой интерпретации?

Т.е допустим мы должны нечто интерпретировать, пускай это даже линейный список некоторых конструкций. Как можно ухитриться сделать так, что бы элементы этого списка были не конструкторами какого-то типа, а чем-то самостоятельным, с определенными, допустим, тайпклассами. Т.е что бы можно было увеличивать количество интерпретируемых элементов. @qnikst вы что-то подобное делали для графов?

через экзестенциальные типы и словари

т.е сериализовывать это всё будет довольно уныло, я так понимаю.

между чем и чем передаваться будет?

если есть single executable или грузится общий модуль то можно через static pointers

допустим, single executable

но храниться выражения должны в... хранилище.

каком-то.

Т.е допустим мы должны нечто интерпретировать, пускай это даже линейный список некоторых конструкций. Как можно ухитриться сделать так, что бы элементы этого списка были не конструкторами какого-то типа, а чем-то самостоятельным, с определенными, допустим, тайпклассами. Т.е что бы можно было увеличивать количество интерпретируемых элементов. @qnikst вы что-то подобное делали для графов?

Ничего не понял, но ассоциации две 1) Data Types a la Carte (Swierstra) 2) Finally Tagless (Kiselyov)

давай без этого, если ты все еще на канале.

но храниться выражения должны в... хранилище.

если single executable по Статик поинтер это пара циферок

давай без этого, если ты все еще на канале.

Сорян, реклама разозлила

ок

Т.е допустим мы должны нечто интерпретировать, пускай это даже линейный список некоторых конструкций. Как можно ухитриться сделать так, что бы элементы этого списка были не конструкторами какого-то типа, а чем-то самостоятельным, с определенными, допустим, тайпклассами. Т.е что бы можно было увеличивать количество интерпретируемых элементов. @qnikst вы что-то подобное делали для графов?

можешь скинуть какой-нибудь минимальный пример я нарисую решение

неа, пока не могу. но примерно это интерпретатор лиспа (секспов), каждая новая конструкция должна добавляться отдельно

fare-name wtf111 base-price usd 35 margin-rate 1.25

непонятно зачем в интерпретаторе динамические сущности. речь ведь про хранение ast?

шоб добавлять в разных модулях например

ну и просто в одном типе я и так умею

ну и просто в одном типе я и так умею

Ну это понятно. про экзистенциальные типы уже сказали и там вроде бы всё ок с ними

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

хотя делал, но в эрланге.

шоб добавлять в разных модулях например

речь про красоту кода (ну то есть один конструктор логически относится к одному модулю и только к нему) или требуется прямо таки новая семантика

но там просто свои парсер-комбинаторы были

ок понятно более менее

хотя тут тоже этим кончится.

А кроме обозначенной проблемы, всё остальное ок? например не получится ли так что придётся перекомпилировать хаскельный интерпретатор для добавления команд

или ты собираешься делать интерпретатор как что-то вроде ghci, но со своим синтаксисом? (интересно насколько сложно сделать ghci, навряд ли в хаскеле есть просто команда eval)

ну,

а зачем мне eval?

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

на самом деле мне скорее интересно, кто как такое делал или может видел

что бы самому не придумывать

Ну

а хотя не. нечего написать

еще у Олега было

про sql

щас найду

а не прям щас не найду

Finally, Safely-Extensible and Efficient Language-Integrated Query

это оно?

да

там близко к этому

но там же на Ocaml

http://okmij.org/ftp/meta-programming/quel.pdf