помогите выбрать ЯП

Ну так это же все равно не горячая замена.

Да, в какой-то степени ты прав - полностью ничем не ограниченной горячей замены нет, потому что она бы легко разрушила типовую консистентность. Но есть возможность - 1) редактировать код в модуле (= файле = буфере) / модулях и запускать новый сеанс GHCi, технически это не горячее обновление, а очередная итерация раздельной компиляции (которая успешна только при правильных типах) с запуском REPL-а для новой версии приложения; 2) в независимых друг от друга сеансах GHCi между (1) проводить какие-то тесты и уже по-настоящему обновлять крутящееся приложение в тех его частях где это разрешено (где есть мутабельность - переменные, STM и т.п.).

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

Почему?

Потому что это просто раздельная компиляция с тайпчеком по всем измененным функциям с последующим подключением нового REPL-а.

Когда они суются в частичные функции потому что на место ненулевых чисел попадает 0 - это не менее печально.

Если 0 : N (или Z) и N (Z) это ADT, а функции тотальны, то никаких ошибок (в виде исключений) деления на ноль не будет.

Но лучше же замести проблему под ковер при помощи _|_ и сделать хорошую мину при плохой игре.

Опять же - это следствие наличия в хаскеле неалгебраических типов и частичных функций (в Agda, например, эта проблема решается - там категория Set, т.е. только тотальные функции). При проектировке своих типов и функций (т.е. приложения) можно избавиться от обсуждаемых проблем используя только алгебраические типы и только тотальные функции. Исключения останутся в нижней части приложения за которую мы не несём ответственности (неалгебраические типы языка, I/O, прочие системные функции).

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

С опционально подключаемой систомой типов/контрактами? Не хочу статику как частный случай динамики, хочу наоборот - это по крайней мере «правильно» :)

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

Только потом, когда уже переписали, вместо «остановить приложение, скомпилировать новую версию, заменить, запустить» мы просто вносим изменение в работающий образ.

Ну да. Если написали без возможности обновлять - обновить без остановки не получится.

Пока хаскидебил чтото компилирует, парсит ошибку чекера и пытается понять - о чем это вообще, я уже запустил тест, нашел эту ошибку и исправил ее.

Если лиспо-гуру vs хаски-дебил, то всё так. Если наоборот - наоборот. Остаётся только перейти на личности и назвать кого-то дебилом :)

Это уже не говоря о том, что чекер статического ЯП работает фундаментально неверно - вместо того, чтобы отвергать код _некорректность_ которого доказана, он отвергает код, для которого не может доказать _корректность_.

Аргументация по Степанову детектед. Можно начинать с типов (интерфейсов, классов, структур данных, аксиом) и заканчивать функциями (реализациями, методами, процедурами, доказательствами) - top-down. Либо наоборот - down-top. Если точно знать что нужно получить (спецификация, интерфейс), то можно начать и с типов, но если представление об этом туманное - можно начать с отдельных функций. Только не понятно, что мешает начать с функций в хаскеле - NoMonomorphismRestriction, поменьше ad-hoc полиморфизма и вперёд.

Еще раз - переписывать _правильную_ программу, чтобы тупой чекер ее пропустил.

Примеры таких программ будут?

Потому что это просто раздельная компиляция с тайпчеком по всем измененным функциям с последующим подключением нового REPL-а.

То есть обычный перезапуск приложения. И при чем тут горячая замена?

Если 0 : N (или Z) и N (Z) это ADT, а функции тотальны, то никаких ошибок (в виде исключений) деления на ноль не будет.

А если бы у бабушки был хуй - то она бы была дедушкой.

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

Нельзя. Система типов слишком невыразительна.

С опционально подключаемой систомой типов/контрактами?

Зачем?

Ну да. Если написали без возможности обновлять

А на практике оно всегда так и есть.

Можно начинать с типов ...

Это к чему все?

Если точно знать что нужно получить (спецификация, интерфейс)

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

Примеры таких программ будут?

Легко:

Prelude> map show [1, "gfdf"]

<interactive>:1:10:
    No instance for (Num [Char])
      arising from the literal `1' at <interactive>:1:10
    Possible fix: add an instance declaration for (Num [Char])
    In the expression: 1
    In the second argument of `map', namely `[1, "gfdf"]'
    In the expression: map show [1, "gfdf"]
Prelude>

Легко

Прикольно. Это про перегруженную show на гетерогенных списках?

Это про то, что списки не гетерогенные. При чем тут show вообще?

Легко: (...)

Эта программа валидна только в твоим мокрых фантазиях лиспоёбка.

Это про то, что списки не гетерогенные.

Что мешает взять гетерогенные?

Она валидна, достаточно поменять тип map.

Взять-то, конечно, можно, вот только система типов, по-моему, слабовата. Так что написать map для гетерогенных списков в хаскеле нельзя.

Ну давай, напиши тип мапа, при котором этот кусок будет валиден.

Use existential types, Luke

То есть написанного типа для map'а я не дождусь?

map :: forall b. (forall a. (Show a) => (a -> b)) -> [exists a. (Show a) => a] ->

Ударился, да?

Нет. А в чем проблема?

Странно, что ещё никто не предложил лисп или схему.

Нет. А в чем проблема?

t1 = map id (1, "2")
t2 = map show (1, "2")

map :: ?
map = ?

Ну я же сразу написал - для каждого тайпкласса нужен свой map (+ отдельный map для exists a. a), т.к. полиморфизма на уровне типов в хаскеле нет и абстрагироваться от тайпкласса как-то так: FORALL T. forall a. (T a) => a -> a, мы не можем. Соответственно, в хаскеле невозможно написать map для гетерогенных списков (без dynamic). Но изначально предложенный код (с show) работать будет, причем сам map переписывать не надо.

Но изначально предложенный код (с show) работать будет, причем сам map переписывать не надо.

Т.е. возможно написать такой map, что с map show (1, «2») всё будет хорошо?

Т.е. возможно написать такой map, что с map show (1, «2») всё будет хорошо?

Зачем писать? Он и так написан - это обычный map. Ему надо только тип поменять.

Зачем писать? Он и так написан - это обычный map. Ему надо только тип поменять.

Вот у меня как-то не получилось оформить такой map. Т.е. map для гетерогенных (,) :: * -> * -> *; (,) :: forall a b. a -> b -> (a, b). К слову, в hlist, функции hMap* тоже ничего не умеют - ни параметрического, ни ad-hoc полиморфизма, ни классов типов.

от у меня как-то не получилось оформить такой map. Т.е. map для гетерогенных (,) :: * -> * -> *; (,) :: forall a b. a -> b -> (a, b).

А, что-то я проглядел, у тебя map для пар? Выше речь о map для списков шла.

Выше речь о map для списков шла.

Там было [1, «gfdf»], т.е. имелись ввиду гетерогенные списки - как раз пары. Для обычных гомогенных списков можно, конечно, делать [VariantType] и писать [N 1, S «2»], [ExistentialType] - [pack 1, pack «2»], [Dynamic] - [toDyn 1, toDyn «2»], и продолжать использовать всё из Data.List.

Там было [1, «gfdf»], т.е. имелись ввиду гетерогенные списки - как раз пары.

Нет, имелись ввиду именно гетерогенные списки, а не пары, то есть [forall a. (T a) => a]

[ExistentialType] - [pack 1, pack «2»]

Об этом речь и шла, проблема только в том, что для каждого тайпкласса (и даже для каждого набора тайпклассов) нужен свой собственный тип для map. Ну и pack в случае полноценной поддержки экзистенциальных типов не нужен, то есть можно просто [1, «2»].

Java.

Нет, имелись ввиду именно гетерогенные списки, а не пары, то есть [forall a. (T a) => a]

Ну, это всё-таки гомогенные списки упакованных значений (хоть в варианты, хоть в экзистенциальные типы, хоть в Dynamic). Следуя лисповой терминологии, или терминологии _h_list - гетерогенные списки кодируются как пары (со стиранием типов в лиспе и сохранением в hlist).

Ну и pack в случае полноценной поддержки экзистенциальных типов не нужен, то есть можно просто [1, «2»].

В haskell нет такой поддержки?

hlist

Но забавно, что такая ерунда это (типа) Ph. D. topic и там есть paper на эту тему.

Ну, это всё-таки гомогенные списки упакованных значений (хоть в варианты, хоть в экзистенциальные типы, хоть в Dynamic).

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

В haskell нет такой поддержки?

Ну в теории, наверное, есть, но когда я попытался сделать [forall .a a], то получил что-то на счет impredicative polymorphism, который давным-давно deprecated, не знаю стоит ли это считать поддержкой или нет. Подключение же указанного расширения дало какую-то невнятную ошибку на счет неоднозначности типов, и что с этим делать - я не понял. Понятно, что надо было куда-то добавить какие-то аннотации, но хрен его знает куда и какие.

Нет, имелись ввиду именно гетерогенные списки, а не пары, то есть [forall a. (T a) => a]

Это не гетерогенные списки. Если бы был exists, то [exists a. T a => a] было бы гетерогенным списком.

Во-первых, exists нет; во-вторых, даже при существующем exists получается parse error.

[exists a. T a => a]

да

Во-первых, exists нет;

ну в ghc нет, и?

даже при существующем exists получается parse error.

с чего вдруг?

И в ghc нет, и в стандарте нет.

> даже при существующем exists получается parse error.

с чего вдруг?

Ты видел вообще ту хуиту, что ты написал? Дай-ка напомню:

map :: forall b. (forall a. (Show a) => (a -> b)) -> [exists a. (Show a) => a] ->

Ты очень слаб. Иди с мельниц^Wплюсами воюй.

Ты видел вообще ту хуиту, что ты написал?

А, ок. На конце не скопипастил, охренеть какая опечатка. Неужели самому нельзя было пофиксить?

И в ghc нет, и в стандарте нет.

И что дальше? Как это отменяет тот факт, что map с указанным типом (map :: forall b. (forall a. (Show a) => (a -> b)) -> [exists a. (Show a) => a] ->) будет вполне корректно работать на списках вроде [1, «2»]?

блять вот такой должен быть тип:

map :: forall c. (forall a. (Show a) => (a -> c)) -> [exists a. (Show a) => a] -> [c]

map :: forall c. (forall a. (Show a) => (a -> c)) -> [exists a. (Show a) => a] -> [c]

Это he2ho. mapShow - для Num нужен mapNum, для id ещё другой map, для he2he ещё другие функции - неюзабельно.

mapShow - для Num нужен mapNum

Я об этом с самого начала сказал - для каждого тайпкласса нужен свой map. Если бы в хаскеле был полиморфизм на уровне типов, можно было бы написать как-то так:

map :: forclass T. forall c. (forall a. (T a) => (a -> c)) -> [exists a. (Show a) => a] -> [c]

но хаскель в такой полиморфизм не умеет. Так что map на гетерогенных списках для любителей статической типизации на данный момент - несбыточная мечта и тема для Ph.D :)

Так что map на гетерогенных списках для любителей статической типизации на данный момент - несбыточная мечта и тема для Ph.D :)

Да тут элементарщина на самом деле - (id 1, id «2») vs. ((\f -> (f 1, f «2»)) id) (почему так?). Слишком рано фиксируется тип полиморфной функции - иначе можно было бы легко использовать (,) :: * -> * -> * как точечные пары и реализовать на этой основе то же что и в Data.List, но гетерогенное.

(почему так?)

потому что forall a b. (a -> a) -> b и forall b. (forall a. a -> a) -> c - разные типы. Но проблему-то это не решает, проблема в том, что для полиморфного типа forall a. (T a) => ... тайпкласс T должен быть фиксирован. Так что в случае ((\f -> (f 1, f «2»)) id) мы просто можем нужный тип указать, а вот в случае гетерогенный списков - мы его указать не можем, нужны разные версии map. То есть нам надо, чтобы ограничение тайпкласса полиморфным было, а не сам тип.

Но проблему-то это не решает

Это бы решило проблему:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, TypeFamilies #-}

import Prelude hiding ( ($), map )

class Apply f a r | f a -> r where
  ($) :: f -> a -> r

instance (a ~ a', b ~ b') => Apply (a -> b) a' b' where
  f $ x = f x

class Map f t t' | f t -> t' where
  map :: f -> t -> t'

instance Map f () () where
  map _ _ = ()

instance (Apply f a a', Map f t t') => Map f (a, t) (a', t') where
  map f ~(x, xs) = (f $ x, map f xs)

и я могу писать:

map (+ 1) (1, (2, (3, ())))
-- > (2,(3,(4,())))

map id (1, (2, (3, ())))
-- > (1,(2,(3,())))

map show (1, (2, (3, ())))
-- > ("1",("2",("3",())))

(никаких заморочек непосредственно с Num, Show etc.) но не могу:

map id (1, ("2", (3, ())))
-- > ...

map show (1, ("2", (3, ())))
-- > ...

последние ничем не отличаются от ((\f -> (f 1, f «2»)) id) и ((\f -> (f 1, f «2»)) show) - тупо не работают.

Это бы решило проблему:

Не решило бы. Потому что:

((\f -> (f 1, f «2»)) id) и ((\f -> (f 1, f «2»)) show) - тупо не работают.

Прекрасно работают. А вот если ты захочешь вместо (\f -> (f 1, f «2»)) применить какую-то функцию-параметр - уже не будет работать без указания конкретного тайпкласса.

Прекрасно работают.

Нет - вот я беру любое из этих выражений, вбиваю в ghci, или компилирую в модуле с помощью ghc --make - не компилируется -> не работает. Если «прекрасно работают» то show me the code.

[code] {-# LANGUAGE RankNTypes, ExistentialQuantification #-}

data Pack = forall a. Pack a n = ((\f -> (f $ Pack 1, f $ Pack «2»)) id) [/code]

Это уже другой код :)

ну GHC не умеет в exists, Если есть exists, можно обойтись без Pack и будет такой же код.