Это core lint failures и полная неюзабельность промоутных GADT-ов (main selling point of TypeInType).

Я его включаю для кайнд-синонимов

А что-то толковое выжать на данный момент трудно.

и то, что я недавно нашел странную вещь * :: * - не баг, это новая фича - первая фаза внедрения завтипов

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

Add * :: *. Why do this? One alternative is to go the route of Coq and Agda and have an infinite tower of type universes. But, this adds a lot of complexity. These languages take this route because * :: * makes a language inconsistent as a logic. However, Haskell is already inconsistent as a logic (because of undefined and GHC.Exts.Any) and so we don't have to worry about a new source of inconsistency. Очень нравится этот абзац.

Не, все очень хорошо, это правильный дизайн для Haskell

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

Даже в Agda сначала иногда с --type-in-type доказываешь для удобства, потом делаешь нормально.

Но с type in type можно доказать что угодно

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

Это мощность типа?

Нельзя

Но с type in type можно доказать что угодно

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

Add * :: *. Why do this? One alternative is to go the route of Coq and Agda and have an infinite tower of type universes. But, this adds a lot of complexity. These languages take this route because * :: * makes a language inconsistent as a logic. However, Haskell is already inconsistent as a logic (because of undefined and GHC.Exts.Any) and so we don't have to worry about a new source of inconsistency. Очень нравится этот абзац.

Though this causes inconsistency in other dependently-typed languages, it does not in Haskell, essentially because equality proofs are written in a different sub-language than ordinary terms. See ​our paper [http://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf] for more details.

А в Хаскеле пруфы надо редьюсить до NF

Это мощность типа?

ну там пример про множества, не про типы, логика кванторов та же, полагаю

Ну в рантайме у тебя уйдет в цикл, а так будто боттома не было.

От этого ты 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?