От этого ты unsafeCoerce не получишь, и на том ладно

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

Хоть Type:Type сделали бы, заживём.

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

Ну вот и не в этом смысл

Для Хаскелиста смысл в том, чтобы сигму и пи получить

а доказывать что-то серьезное небось никто и не будет

(а кто будет об этом пожалеет)

У тебя предположение, что есть proof erasure.

Это называется изоморфизмом харри-ховарда (населённые типы это истинные утверждения)

Я не про то

Вот если у тебя есть let x = x in x :: Void, ты зафорсишь в рантайме и уйдешь в цикл, и никакой False ты в рантайме не доказал

так же и с Жираром

составишь циклящийся тёрм, а в рантайме-то тебе что с того?

По-моему произошло что-то очень странно и программисты стали воспринимать зависимые типы как ещё один способ полиморфизма >...>

@int_index, нужна пи и сигма это про это

парадокс Жирара основывается на тёрме без нормальной формы

если нет proof erasure и в рантайме для доставания пруфа делается NF, то уйдешь в цикл

это просто еще один боттом, к которым все в Хаскеле привыкли и смирились

делать иерархию универсумов без тоталити чекера не надо никому

а делать тоталити чекер для Хаскеля в 300 раз амбициознее, чем DependentHaskell

а сигма и пи полезны и с Type:Type

Составь Refl :: Int :~: Bool с Type:Type, тогда можно паниковать

а я утверждаю, что ты составишь только bottom :: Int :~: Bool

и никому от этого ни горячо, ни холодно

потому что я и без того могу: sueMe :: Int :~: Bool sueMe = sueMe

только GHC требует матчнуть на этой штуке: oops :: a :~: b -> a -> b oops Refl = id

и если ты сделаешь oops sueMe, то ты получишь не unsafeCoerce, а цикл

вот это рассуждение вообще заложено в основу дизайна DependentHaskell, и это хороший, прагматичный подход

Вы по-моему меня не понимаете. Мой тезис в следующем: пи и сигма нужны только как инструменты доказательства тотальности. А иметь в языке пи, сигму "просто чтобы было" особо никому и не нужно. Просто ещё одна возможность сделать что-то неправильно

А это в корне неверный тезис

Почему?

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

Которые будут вполне реально обеспечены пока пруфтёрмы редьюсятся в NF

Женя, согласен?

например exist n : M, even(n) -> |M| > 0 = (forall n : M, even(n)) -> |M| > 0 тут же первое утверждение верное, а второе нет.

А почему второе утверждение неверное? Импликации ни тепло ни холодно от заведомо ложной посылки.

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

А пример можно?

А пример можно?

printf :: (s :: String) -> PrintfParams s -> IO ()

printf "Result is %f with %d accuracy" :: (Double, Integer) -> IO ()

printf "Hello, World" :: () -> IO ()

в общем как в Си, только тайпсейф за счёт Пи

ты про singletons? Да, все эти костыли для эмуляции завтипов я видел ранее, а тут прям что-то реальное делается, только без универсумов

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

товарищи, а кто такой LDouble?

товарищи, а кто такой LDouble?

inline-c?

hsc2hs

ну я только тут видел https://www.stackage.org/haddock/lts-10.0/inline-c-0.6.0.5/Language-C-Types.html#v:LDouble

if test "$HTYPE_IS_FLOAT" -eq 1 then AC_CV_NAME=Float elif test "$HTYPE_IS_DOUBLE" -eq 1 then AC_CV_NAME=Double elif test "$HTYPE_IS_LDOUBLE" -eq 1 then AC_CV_NAME=LDouble else AC_CV_NAME_supported=no fi

не это не то

#define hsc_type(t...) \ if ((t)(int)(t)1.4 == (t)1.4) \ hsc_printf ("%s%lu", \ (t)(-1) < (t)0 ? "Int" : "Word", \ (unsigned long)sizeof (t) * 8); \ else \ hsc_printf ("%s", \ sizeof (t) > sizeof (double) ? "LDouble" : \ sizeof (t) == sizeof (double) ? "Double" : \ "Float");

#type C_type A Haskell equivalent of the C numeric type will be output. It will be one of {Int,Word}{8,16,32,64}, Float, Double, LDouble.

long double? (10 bytes)

S

/stat@combot

combot.org/chat/-1001043143583

Alo

https://ghc.haskell.org/trac/ghc/ticket/12919 https://ghc.haskell.org/trac/ghc/ticket/12564

почему странно?

А почему второе утверждение неверное? Импликации ни тепло ни холодно от заведомо ложной посылки.

А кто нибудь использует VS Code для разработки?

иногда

А кто нибудь использует VS Code для разработки?

да

А кто нибудь использует VS Code для разработки?

да

да

@qnikst ты завязал с вимом?

смог выйти

Какой набор расширений используете? Работает ли Jump to definition?

ERROR: S client not available

@qnikst ты используешь vs code ?!

btw, есть ли редакторы кроме вима и емакса, на которые стоит посмотреть в 2017 - 2018 ? (последняя попытка перейти на емакс была примерно пять лет назад)

emacs + evil-mode 8)

evil mode у меня и так есть, а нужен ли к нему емакс я пока не понял

evil-mode это в смысле вим в емаксе

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

конечно

btw, есть ли редакторы кроме вима и емакса, на которые стоит посмотреть в 2017 - 2018 ? (последняя попытка перейти на емакс была примерно пять лет назад)

vscode

в емаксе намного проще воркфлоу

перелез на него с вима, потому что вим тормозил)

vs - это же вижуал студио?

ну вот я перебрался уже примерно 3 года назад. Обратно в вим захожу по привычке, но там же по привычке жму емаксовые хоткеи и от этого иногда страдаю

нет

vs - это же вижуал студио?

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

ну то есть vscode не имеет ничего общего с просто vs

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

это https://code.visualstudio.com/ ?

да

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

только намного шустрее и удобнее атома

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

в первую очередь эскейпа

индусы продают майрософт столлману и торвальдсу, репин, ascii-арт

А кто нибудь использует VS Code для разработки?

да, hie

@qnikst ты используешь vs code ?!

нет конечно

но там было про кто-нибудь

поздно, я уже его поставил

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

даже подсветка синтаксиса

Его Кметт использует

ну так редактор для js-а на js-е

(для C++)