IDE для Haskell - когда появится?

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

Толсто.

Байтоложество - это работа с голой памятью. Она в хаскеле есть, но в очень ограниченных количествах, почти всегда на стыке с FFI. В повседневной жизни её нет. Оптимизация haskell'ного кода ни к какой работе с памятью не сводится. Всякие там уменьшения числа кэш-промахов можно сделать только вынесением части алгоритма в C, насколько я представляю.

Толсто.

Мне правда интересно было бы услышать контрпример.

okay, принято. Я подозреваю что отладка (профилирование) хаскельного кода на порядок сложнее починки сегфолтов, но спорить не буду, тк недостаточно знаком с предметом.

если программа и падает, то сообщение об ошибке всегда читаемое

Например, где-то применяется head к пустому списку. Всё, что ты увидишь, это

*** Exception: Prelude.head: empty list

Где конкретно это произошло, непонятно.

Смотреть содержимое переменных не нужно, ибо их нет.

Есть выражения и биндинги. И даже «переменные» переменные: MVar, STRef и прочее.

И даже «переменные» переменные: MVar, STRef и прочее.

Так и знал, что кто-нибудь об этом скажет. Называть их переменными я бы не стал. Для простоты: монада State - это действительно мутабельные данные? Вроде похоже, а на самом деле внутри ничего, кроме чистого кода нет. Имхо, это скорее эмуляция переменной.

Про исключения согласен, мне что-то казалось, что место, где они выбрасываются, тоже пишется, но можно так:

┌[pts/1: ~/tmp]
└% ./Fail +RTS -xc
*** Exception (reporting due to +RTS -xc): (THUNK_2_0), stack trace: 
  GHC.List.CAF
  --> evaluated by: Main.a,
  called from Main.CAF
  --> evaluated by: Main.CAF
Fail: Prelude.head: empty list

Называть их переменными я бы не стал.

Но они вполне переменные с in-place обновлением. Нормальная форма (с точки зрения чистой хаскельной семантики) программы с IO и IORef/MVar/... это спецификация компилятору по написанию программы с настоящими эффектами и настоящими переменными - компилятор должен превратить её в библиотечные, системные и rts вызовы сделав из биндингов типов IORef/MVar/... живые (относительно Scheduler/GC/STM/IOManager/...) объекты в памяти с соответствующим поведением.

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

Emacs haskell-mode отлично форматирует код и подсветка вполне норм.

А по поводу автокомплита и прочих мокрых писечек то тут с хаскелем не все так просто. Если ты знаком с системой типов хаскеля, то должен понимать, что одни и те-же буквенные выражения в разных контекстах могут иметь разный тип и абсолютно разную семантику. Чтобы такое реализовать нужен по сути полноценный интерпретатор хаскеля с выводом типов, да не просто интерпретатор, а какой-то инкрементальный или типа того.

Emacs haskell-mode имеет удобную поддержку ghci. Написал код - нажал F5(у меня настроено, сам можешь на другую клавишу забиндить) - и получил сообщение, что все норм, или не норм и сообщение с ошибкой.

А еще в ghci очень удобно просматривать полученные типы функций и проверять работоспособность кода на скорую руку, и много чего еще. Это называется REPL. Попробуй - еще захочешь инфа 100%.

Где конкретно это произошло, непонятно.

И не будет (в общем случае). Ленивость же. Более того, это не исключение в смысле С++ или явы, это особое значение _|_ (bottom). Объект первого класса, то есть. Можно возвращать, передавать в качестве параметра, присваивать и т.д. Чудеса начинаются при попытке его вычислить.

«Классическая» (что бы это значило) отладка в хаскеле еще невозможна потому что хаскель - один громадный кусок синтаксического сахара для скромного и компактного языка - System F (с расширениями). Отлаживать на уровне System F, или его С-- представления или LLVM представления С-- (если задействовано) или машинных кодов ты можешь. Но это не для живых людей.

О! И вдогонку постик про IDE http://michaelochurch.wordpress.com/2013/01/09/ide-culture-vs-unix-philosophy/

Шикарный тред, где стыдно всем.

ты сам-то на хацкеле хоть 5 строчек написал?

*** is a cluster virtual server management software tool built on top of existing virtualization technologies such as Xen or KVM and other Open Source software.

*** requires pre-installed virtualization software on your servers in order to function. Once installed, the tool will take over the management part of the virtual instances (Xen DomU), e.g. disk creation management, operating system installation for these instances (in co-operation with OS-specific install scripts), and startup, shutdown, failover between physical systems. It has been designed to facilitate cluster management of virtual servers and to provide fast and simple recovery after physical failures using commodity hardware

код на haskell есть. При том приходилось его читать и править, код чужой.

Зачем тут IDE? На и нафига тебе вообще было знать эту задачу?

IDE для хацкеля должно быть написано на хацкеле

таки да - хорошая проверка на практичность для ЯП

на самом деле - действительно к черту, поскольку _хороших_ средств отладки нет, во всяком случае я не видел, а во всём комьюнити сложилось мнение что Debug.Trace (и ещё trace помнящий вложенность), при учете вопремя написанных Quick и Unit тестов и логирование - вполне достаточно, чтобы не иметь отладчика, в крайнем случае его можно полностью заменить сессией ghci с дополнительными пакетами, типа heap-view и т.п.

это спецификация компилятору по написанию программы с настоящими эффектами и настоящими переменными

Поэтому мне всё-таки кажется, что MVar - не переменная, а скорее чисто функциональная конструкция, вызов библиотечной функции «сгенерировать код, ведущий себя как обращение к переменной».

Надеюсь, не слишком заблуждаюсь, внутренности IO я пока слабо представляю.

Т.е. правильно ли я понимаю, что и всю IO можно реализовать с помощью абсолютно чистого кода, с единственным исключением для unsafe функций вида IO a -> a, внутри которых происходит некая императивная магия, и которые, вообще говоря, не могут быть написаны на haskell? Это, наверное, было бы печально по производительности, просто в порядке мысленного эксперимента.

И не будет (в общем случае). Ленивость же. Более того, это не исключение в смысле С++ или явы, это особое значение _|_ (bottom). Объект первого класса, то есть. Можно возвращать, передавать в качестве параметра, присваивать и т.д. Чудеса начинаются при попытке его вычислить.

Что такое bottom, я в курсе. Но цепочку вычислений, приведшую к попытке вычислить bottom, проследить можно же.

«Классическая» (что бы это значило) отладка в хаскеле еще невозможна потому что хаскель - один громадный кусок синтаксического сахара для скромного и компактного языка - System F (с расширениями). Отлаживать на уровне System F, или его С-- представления или LLVM представления С-- (если задействовано) или машинных кодов ты можешь. Но это не для живых людей.

Ага, а Java тогда — это синтаксический сахар для Jаva-байткода.

тяжеловесного

Имеются в виду его 100500 библиотек. Их же нельзя все выучить, что ты )

Хотя бы реализовывать на нем проекты сложнее фракталов и хелловорлда.

А IDE тут при чем? Ей же пофиг что парсить, я думал вы в этом смысле говорите

Т.е. правильно ли я понимаю, что и всю IO можно реализовать с помощью абсолютно чистого кода, с единственным исключением для unsafe функций вида IO a -> a, внутри которых происходит некая императивная магия, и которые, вообще говоря, не могут быть написаны на haskell?

Вычислительные возможности любого чистого функционального языка таковы, что в нём можно смоделировать память и всю IO, в том числе run :: IO a -> a. Например

module IOSemantic where

open import Function
open import Data.Unit hiding ( _≟_ )
open import Data.Bool hiding ( _≟_ )
open import Data.Nat
open import Data.Fin hiding ( _+_ )
open import Data.List
open import Data.Product
open import Relation.Nullary

module MemoryModel (Data : Set) (zero : Data) where

  Size : Set
  Size = ℕ

  Index : Size → Set
  Index = Fin

  Memory : Size → Set
  Memory size = Index size → Data

  updateMemory : ∀ {size} → Index size → Data → Memory size → Memory size
  updateMemory i d a j with (toℕ i ≟ toℕ j)
  ... | yes _ = d
  ... | no _  = a j

  Shape : Set
  Shape = List Size

  data Heap : Shape → Set where
    Empty : Heap []
    Alloc : {shape : Shape} {size : Size} → Memory size → Heap shape → Heap (size ∷ shape)

  data Location : Shape → Size → Set where
    Top : {shape : Shape} {size : Size} → Location (size ∷ shape) size
    Pop : {shape : Shape} {size size′ : Size} → Location shape size → Location (size′ ∷ shape) size

  updateHeap : ∀ {shape size} → Location shape size → Index size → Data → Heap shape → Heap shape
  updateHeap Top     i x (Alloc a h) = Alloc (updateMemory i x a) h
  updateHeap (Pop k) i x (Alloc a h) = Alloc a (updateHeap k i x h)

  lookup : ∀ {size shape} → Location shape size → Index size → Heap shape → Data
  lookup Top     i (Alloc a _) = a i
  lookup (Pop k) i (Alloc _ h) = lookup k i h

  data IO (A : Set) : {_ _ : Shape} → Set where
    Pure  : {shape : Shape} → A → IO A {shape} {shape}
    New   : {shape shape′ : Shape} → (size : Size) → (Location (size ∷ shape) size → IO A {size ∷ shape} {shape′}) → IO A {shape} {shape′}
    Read  : {shape shape′ : Shape} {size : Size} → Location shape size → Index size → (Data → IO A {shape} {shape′}) → IO A {shape} {shape′}
    Write : {shape shape′ : Shape} {size : Size} → Location shape size → Index size → Data → IO A {shape} {shape′} → IO A {shape} {shape′}

  return : ∀ {A shape} → A → IO A {shape} {shape}
  return = Pure

  infixr 0 _>>=_

  _>>=_ : ∀ {A B shape shape′ shape′′} → IO A {shape} {shape′} → (A → IO B {shape′} {shape′′}) → IO B {shape} {shape′′}
  Pure x         >>= f = f x
  Write a i x wr >>= f = Write a i x (wr >>= f)
  Read a i rd    >>= f = Read a i (λ x → rd x >>= f)
  New n io       >>= f = New n (λ a → io a >>= f)

  infixr 0 _>>_

  _>>_ : ∀ {A B shape shape′ shape′′} → IO A {shape} {shape′} → IO B {shape′} {shape′′} → IO B {shape} {shape′′}
  io >> io′ = io >>= const io′

  run : ∀ {A shape shape′} → IO A {shape} {shape′} → Heap shape → A × (Heap shape′)
  run (Pure x)       h = x , h
  run (Read a i rd)    h = run (rd (lookup a i h)) h
  run (Write a i x wr) h = run wr (updateHeap a i x h)
  run (New n io)       h = run (io Top) (Alloc (λ i → zero) h)

  new : ∀ {shape} → (size : Size) → IO (Location (size ∷ shape) size)
  new n = New n Pure

  write : ∀ {shape size} → Location shape size → Index size → Data → IO ⊤
  write arr i x = Write arr i x (Pure tt)

  read : ∀ {shape size} → Location shape size → Index size → IO Data
  read arr i = Read arr i Pure

open MemoryModel ℕ 0

test : IO ℕ {[]}
test =
  new 2 >>= (λ x →
  -- two zeroed memory cells here
  write x i 422 >>
  write x ii 244 >>
  read x i >>= (λ a →
  read x ii >>= (λ b →
  return (a + b))))
  where i = zero ; ii = suc zero
--
-- ⇒
--
-- MemoryModel.New 2
-- (λ a →
--    MemoryModel.Write a zero 422
--    (MemoryModel.Write a (suc zero) 244
--     (MemoryModel.Read a zero
--      (λ x →
--        MemoryModel.Read a (suc zero)
--         (λ x' → MemoryModel.Pure (x + x'))))))
-- 

runTest = run test Empty
-- 
-- : ℕ × Heap (2 ∷ []))
-- 
-- ⇒
-- 
-- 666 ,
-- MemoryModel.Alloc
-- (λ j →
--    MemoryModel.updateMemory ℕ 0 (suc zero) 244
--    (λ j' →
--       MemoryModel.updateMemory ℕ 0 zero 422 (λ i → 0) j' | 0 ≟ toℕ j')
--    j
--    | 1 ≟ toℕ j)
-- MemoryModel.Empty
-- 

Это гомогенная модель, гетерогенная получается дописывание маршалинга в Data.

Просто эти чистые вычисления тоже должны где-то проходить, то есть быть реализованы - семантика изменяемой локации будет всегда, но всё-таки лучше, если оно ещё и работать будет с реальной памятью in-place (как GHC и делает, то есть реализует изменяемое состояние в виде переменных).

Хотя бы реализовывать на нем проекты сложнее фракталов и хелловорлда.

Haskell in industry

А еще в ghci очень удобно просматривать полученные типы функций и проверять работоспособность кода на скорую руку, и много чего еще. Это называется REPL. Попробуй - еще захочешь инфа 100%.

Я охотно пользуюсь Scala REPL.

Haskell in industry

грустный список, в основном либо упоминается, что хаскель приткнули для второстепенных задач, вроде генерации байдингов для lua, либо по ссылкам откровенные ноунеймы или тухлый мрак вроде http://www.ansemond.com

google, nvidia, at&t, facebook?

google

Haskell is used on a small number of internal projects in Google

nvidia

in-house tools

at&t

automate processing of internet abuse complaints

facebook

lex-pass is a tool for programmatically manipulating a PHP code base via Haskell.

как я и сказал - «приткнули для второстепенных задач»

А ты пробовал кодировать на Java без IDE?

Тут та же песня.

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

референсная реализация Haskell вместе с набором, скажем так, классических библиотек, откровенно нестабильная; все крупные компании этот риск учитывают

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

Тут та же песня.

голословное утверждение. на Haskell с haskell-mode в emacs лично мне писать удобней, чем на Java в Eclipse. это разные языки

IDE для хацкеля должно быть написано на хацкеле

с хрена ли?

и, они по этому наверное на haskell разработчиков набирают активно? (во всяком случае гуглы, и фэйсбуки, которые Симона Марлоу наняли)

и, они по этому наверное на haskell разработчиков набирают активно?

смотря что понимать под «активно», для корпорации вроде google, которая пилит свои ЯП ради лулзов, «активно» - это сотни и тысячи вакансий, покажи их

ну или хотя бы 5-10, уровень мелкой шарашки, но как «пруф» сойдет

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

вакансий и предложений, о которых я знаю

не покажешь значит :(

блин, сам гугли их вакансии в Дублинском, Лондонском и Московском офисах, вот честно, я даже не знаю, где у них эти линки искать =)

блин, сам гугли

хороший ответ, часто используется

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

а какая разница? мне не надо - другие прочитают, да и не я вообще затронул тему вакансий, это ты сделал громкое заявление без пруфов

agda я не знаю, но там написана некая модель линейного куска памяти? Т.е. это просто вариация на тему State Monad? Имелось в виду, что этот код можно (?) научить работать с настоящей памятью и он будет совершать «настоящие» побочные эффекты, вроде ввода-вывода и т.д?

семантика изменяемой локации

Не смог нагуглить этот термин.

кому интересно и так знают где искать, и многие из перечисленных фирм не считают нонеймами, а ещё можно и off-the-lor спросить.

я уже понял, что пруфа не будет, и ничего не имею против - нет так нет

там написана некая модель линейного куска памяти?

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

Для простоты возьмём язык из последовательного выполнения, значений, чтения и записи значений по адресам в плоской памяти. Такой язык можно перечислить как ADT:

data Imp addr val res
  = Return res
  | Write addr val (Imp addr val res)
  | Read addr (val -> Imp addr val res)

Теория предполагается. Дальше, термы этого языка можно писать обычным функциональным кодом (будем считать что pure & LC based):

write :: addr -> val -> Imp addr val ()
write addr val = Write addr val $ return ()

read :: addr -> Imp addr res res
read addr = Read addr return

instance Monad (Imp addr val) where

  return = Return

  Return res >>= f = f res
  Write addr val imp >>= f = Write addr val $ imp >>= f
  Read addr imp >>= f = Read addr (imp >=> f)

Например такой терм:

test :: Imp Integer Integer Integer
test = do
  write 0 2
  write 1 3
  a <- read 0
  b <- read 1
  return $ a + b

то есть нормальная форма test.

Вопрос в том, можно ли построить модель такой теории написать ей big-step семантику в виде функции run в чистом функциональном языке. Для этого достаточно как-то смоделировать плоскую память. Проще всего взять память как функцию из адресов в значения (addr -> val), например (const 0) это занулённая память. Такую память можно обновлять обновлением функции:

update :: Eq addr => addr -> val -> (addr -> val) -> addr -> val
update addr val mem addr' | addr == addr' = val | otherwise = mem addr'

и читать обычной аппликацией:

lookup :: addr -> (addr -> val) -> val
lookup = flip ($)

После этого уже получается интерпретация сохраняющая свойства теории («правильность»):

run :: Eq addr => (addr -> val) -> Imp addr val res -> res
run _ (Return res) = res
run mem (Write addr val imp) = run (update addr val mem) imp
run mem (Read addr imp) = run mem $ imp $ lookup addr mem

runZero :: (Eq addr, Num val) => Imp addr val res -> res
runZero = run $ const 0

-- runZero test => 5

Можно расширять язык Imp другими императивными конструкциями - циклами, условиями и т.д., и дописывать функцию run - всегда будет существовать такая интерпретация.

Т.е. это просто вариация на тему State Monad?

Не совсем. Тут мы начинаем с языка и его свойств, то есть теории - это универсальные вещи, после чего ищем им модель в чистом ФП в виде интерпретации/big-step семантики.

этот код можно (?) научить работать с настоящей памятью и он будет совершать «настоящие» побочные эффекты, вроде ввода-вывода и т.д?

Память и побочные эффекты становятся настоящими когда это FFI, DMA, прерывания и т.п., то есть нечто на тему реальной операционной реализации, а не денотационной абстракции. Вот в GHC термы IO это State над RealWorld, функцию run частично реализует компилятор превращая, например, newIORef/readIORef/writeIORef в реальные операции над единственным для каждого newIORef куском памяти. «Изменяемые локации» есть в State/ST/IO, просто потому что они обладают определёнными _свойствами_ (из подходящего определения «изменяемой локации» в рамках теории). Почему при этом IORef это «переменные»? Потому что они обладают ещё более специфичными свойствами, но уже не с денотационной точки зрения, а с операционной (small-step) и с точки зрения реализации (в терминах которых можно дать определение понятию «переменная с in-place обновлением»).

Не смог нагуглить этот термин.

Имеются в виду те уравнения которые задают определение изменяемой локации в теории императивного языка - у правильной теории будут модели в которых будет находить отражение эта «семантика изменяемой локации».