Анализ пользователей Common Lisp и Racket

class Sum a b where
  type SumResult a b 
  (+) :: a -> b -> SumResult a b

Если только так.

но как я и говорю тут будет участвовать какое-то приденение и возможно куча правил по тому, какой тип будет результатом, например первый в операции, или более широкий, или что ещё. В ООП с subtyping (напр. java как понятный мне) вполне допустимо иметь: Num -> Float -> Complex, и тогда 'A add(A obj);' соотв. при вызове Complex(3).add(Float(5)) ясно, что результат будет Float, а Float(5).add(Complex(3)) не тайпчекнется. Но без subtyping так нельзя.

А введение кучи правил зло, см. си.

Оно на нем выдается? Если да, то имеет.

Не имеет. Еще раз:

strLen x = (+ x)

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

При том что plus1 :: Int -> Int мы её применяем: plus1 1, но это ошибка т.к. это не соответствует специкации в моей голове, что результат должен быть String.

Если в спецификации указано plus1 :: Int -> Int и ты пишешь plus1 1, то все ок. Если спецификации не указано - надо ее потребовать. Если в спецификации указано plus1 :: Int -> String то plus1 1 покажет ошибку. Достаточно указать тип для самой plus1, у применения ничего указывать не нужно.

Я так не утверждал

Именно это ты и утверждал.

а за одно отличать correct от well typed.

Мы весь тред говорим исключительно о корректности. well typed не нужен.

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

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

Prelude> let strLen x = (+ x)
Prelude> let yoba = show . strLen
Prelude> yoba "5"

<interactive>:4:1:
    No instance for (Show ([Char] -> [Char]))
      arising from a use of `yoba'
    In the expression: yoba "5"
    In an equation for `it': it = yoba "5"
Prelude>

это вообще чудесно - оно даже йобу съело и выдало ошибку только на аппликации

Твой вариант её несет нисколько дополнительной информации

То есть адекватные сообщения об ошибках, которые позволяют найти и исправить ошибку в несколько ра быстрее - не несут никакой дополнительной информации? Ну ок, чо.

Нет, я просто опечатался и забыл применить к этому show, а чеккер гад не проверил это. (Если что это калька с вас)

Нет, не калька. Чекер должен проверять соответствие реализации спецификации. Саму спецификацию он проверять не должен (разве что на непротиворечивость), она считается правильной by design.

Ну, например, чтобы рассказывать почему в ракетке есть local type inference и нету module level, не противореча истокам.

Он был, но его убрали, т.к. он давал невменяемые сообщения об ошибках (как в хаскеле).

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

Да нифига (про третье) глобальный вывод типов не может вывести тип больший, чем локальный: (localType >= signature >= inferred type), что я так понимаю не справедливо в случае ракетки.

«величина» типа тут не причем. Смысл в том, что сообщение об ошибке существенно зависти от control-flow самого инференса. В случае полного инференса чекер может показать ошибку очень далеко от места ее возникновения - вплоть до другого модуля (что, собственно, и было не раз продемонстрировано в этом треде). Это свойство инференса - можно всегда подобрать такой ход унификации, что, в случае ошибки, она будет показана в любом наперед заданном месте (хотя проихошла она в месте вполне конкретном). Смысл в добавлении топлевел аннотаций тут в том, что с этими аннотациями ошибка не сможет выйти за пределы ф-и (т.к. унификация работает только внутри). То есть если тебе выводильщик показал ошибку в ф-и Х - она ГАРАНТИРОВАННО в ф-и Х. А не как в хаскеле - где угодно в другом произвольном месте твоего проекта.

2. Третья часть (уточнение типа через то как он используется - отсутвует), есть подозрение что из-за эффектов при subtyping.

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

Насколько я знаю rank2types ещё выводится, а это уже нет.

Тут и есть rank2, стрелочка справа-то одна всего

(+) :: a -> b -> SumResult a b

То есть вместо x + y + z придётся писать fromResult (x + y) + z ?

В C++ в этом смысле удобнее. Там было бы что-то вроде:

plusMyNumFloat :: MyNum -> Float -> Float
plusMyNumFloat = ...
class MyNum where
  (+) :: MyNum x -> Float y -> Float = plusMyNumFloat x y
  (+) :: Float x -> MyNum y -> Float = plusMyNumFloat y x
  (+) :: MyNum -> Int -> MyNum = ...
  (+) :: Int -> MyNum -> MyNum = ...
  ...

Вот это и был бы полиморфизм. Приведения типов (неявного) нет, но под одним именем группа функций.

Задача «найти ошибку и максимально точно указать ее местоположение и характер»

Епт. Чекер ищет ошибки в том, что ты написал, а не в том, что ты хотел написать.

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

Я начинаю понимать, какие чекеры ты писал.

Епт. Чекер ищет ошибки в том, что ты написал, а не в том, что ты хотел написать.

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

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

Ещё раз, медленно и печально: чекер ищет ошибки в том, что ты написал; если ты написал не то, о чем думал, чекер сработает плохо (или даже не сработает вообще).

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

Ничем не плохо. И просто для протокола: я не любитель Хаскела и не защищаю глобальный вывод типов; но кто-то должен был попробовать этот подход и Хаскел, как игрушка академиков, вполне очевидный кандидат. Так что я не понимаю, почему фейл глобального вывода в Хаскеле (если это фейл) так важен - языки, претендующие на статус «промышленных» (Rust, Swift) не используют глобальный вывод.

Ещё раз, медленно и печально: чекер ищет ошибки в том, что ты написал; если ты написал не то, о чем думал, чекер сработает плохо (или даже не сработает вообще).

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

Ничем не плохо.

Если ты согласен что, в хорошем промышленном ЯП лучше не давать фулл инференса, то о чем вообще спор?

Зачем нужен чекер, который в случае наличия ошибки «сработает плохо (или даже не сработает вообще)»

Чтобы сигнализировать, если ты написал то, что подумал, но не так, как нравится компилятору :-)

ошибка - это и есть «написал не то, о чем думал».

Пример, который ты привёл - это вид ошибки, известный как «описка». Нелепая, относительно редкая, и _сразу обнаруженная_.

Зачем нужен чекер, который в случае наличия ошибки «сработает плохо (или даже не сработает вообще)»?

Опять это детство... Да, естественно, чекер может сработать плохо. Но если соотношение плохих и хороших срабатываний 10:1 - это полезный чекер; если 1:10 - бесполезный.

А «не сработает вообще» относилось к случаю, когда ты вместо + напишешь -. Тоже элементарная описка, но вообще не ловится.

Если ты согласен что, в хорошем промышленном ЯП лучше не давать фулл инференса, то о чем вообще спор?

О том, что в хорошем промышленном языке должна быть статическая типизация. И я очень подозревают, что даже локальный вывод иногда выдаёт загадочные сообщения об ошибках.

Чтобы сигнализировать, что в результате ты написал гарантированно некорректную программу.

Пример, который ты привёл - это вид ошибки, известный как «описка». Нелепая, относительно редкая, и _сразу обнаруженная_.

Во-первых, она не обнаружена. Чекер даже не указал модуль правильно. Во-вторых - описки это самые частые ошибки. Другое дело, что они обычно легко ищутся и быстро, просто исправляются. Но данный пример как раз демонстрирует, как фуллиференс может поиск и исправление такой вот тривиальной ошибки превратить в натуральный адъ.

Да, естественно, чекер может сработать плохо. Но если соотношение плохих и хороших срабатываний 10:1 - это полезный чекер; если 1:10 - бесполезный.

О чем и речь. Если инференс глобальный, то соотношение сразу смещается с 10:1 к 1:10. Если ты свои аннотации типов не пишешь, то корректное обнаружение ошибки - исключение, а не правило, потому что унификация может обломиться в сотне разных мест, и вероятность того, что попадется именно на нужно место - резко стремится к нулю.

И я очень подозревают, что даже локальный вывод иногда выдаёт загадочные сообщения об ошибках.

Безусловно. Но «размытость» сообщения в любом случае ниже. Если у нас вывод ограничен топ-левел ф-ей - то ошибка гарантированно будет указана с точностью до топ-левел ф-и. Если модулем - с точностью до модуля. Если ничем - ошибка может быть АБСОЛЮТНО ГДЕ УГОДНО, вне зависимости от того, где ее указал тайпчекер. Ну, то есть, натурально: «в вашей программе ошибка, где-то среди 100мб сорцев» :)

О том, что в хорошем промышленном языке должна быть статическая типизация.

Зачем тогда ты влез в разговор о пользе/вреде глобального инференса? :hz:

Чтобы сигнализировать, что в результате ты написал гарантированно некорректную программу.

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

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

ты прав

То есть вместо x + y + z придётся писать fromResult (x + y) + z ?

не знаю, откуда ты сделал этот вывод :/.. дай угадаю, конструкция associated type with class тебе не известна?

Обьясняю на пальцах, вышеописанный обозначает, что у нас есть двупараметрический класс типов Sum, и с ним связан синоним типа SumResult, который зависит от параметров, например, instance Sum Int Double where SumResult Int Double = Double. Таким образом выражение: 1+3.0+2 будет корректно типизировано и результатом будет Double. Как я писал в C++ неявное преобразование типов, и удобнее ли это вопрос открытый.

Приведения типов (неявного) нет, но под одним именем группа функций.

приведение типов будет в plusMyNumFloat (кстати, во втором кейсе нужно бы было plusMyFloatNum?). К слову мне совершенно неочевиден тип возвращаемый операцией (+).

я, кстати, выше написал, что «глобальный» вывод типов может только уточнить тип функции по месту ее применения и никак не влияет на само определение функции. С поправкой на сабтайпинг в ракетке есть тот же локальный вывод типов, но в отличии от хацкеля сингатуры для топ-левел S-Expressions требуются (в haskell тупо warning). К каким проблемам это может привести мне не сильно очевидно (то, что тут приводят как проблему - это проблема в днк авторов кода).

лисперы! да вы издеваетесь про опечатки

не тайпчекается

(define (show x)
  (if (number? x)
      (number->string x)
      ("not yet implemented")))

тайпчекается

(define (show x)
  (if (number? x)
      (number->string x)
      "not yet implemented"))

хорошо хотя бы ошибку по месту пишет.

со стороны Haskell статей не читал

O'Haskell (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.6215)?

А так можно эмулировать классами / фантомными типами.

http://research.microsoft.com/pubs/67441/overloading_conf.pdf

http://okmij.org/ftp/Haskell/HList-ext.pdf

instance Sum Int Double where SumResult Int Double = Double

Да. Понял. Кстати, (+) от Num и (+) от MyNum в одном модуле сосуществовать смогут или нет?

приведение типов будет в plusMyNumFloat

Почему это? У неё два аргумента MyNum и Float. Одно к другому не приводится.

кстати, во втором кейсе нужно бы было plusMyFloatNum

Там порядок аргументов другой, функция та же.

К слову мне совершенно неочевиден тип возвращаемый операцией (+).

В зависимости от типов аргументов (в этом смысл полиморфизма). В принципе SumResult даёт тот же эффект. Открытый вопрос только про одинаковые операции в разных тайпклассах. Если можно, то тогда действительно не хуже C++ в этом плане.

тайпчекается

А что не так? Any->String

В haskell

data T = Number Int | Any String | Anything

show' (Number x) = show x
show' x = "not implemented"

Тоже тайпчекается. Или что ты от него хотел (какая опечатка имелась в виду?)?

Кстати, (+) от Num и (+) от MyNum в одном модуле сосуществовать смогут или нет?

импортированные квалифицировано - смогут. Только не надо так делать, в силу неиньективности type families к чертям type inference поломаешь, т.к. из-за неиньективности та часть, против которой вы тут ругаетесь не будет работать - и это уже неудобно.

Почему это? У неё два аргумента MyNum и Float. Одно к другому не приводится.

в модели с subtyping - возможно.

Если можно, то тогда действительно не хуже C++ в этом плане.

можно в посмотреть плюсовый код где add(int, double) -> double, add(rational, float) -> double, add(int, int) -> int? =)

мне не нравится то, что код отличается наличием скобочек вокруг «not implemented». (Я конечно не читал reference, но предполагал, что скобочки это исключительно инструмент выделения блоков).

К каким проблемам это может привести мне не сильно очевидно

Еще раз для особо одаренных - проблема состоит в том, что вместо указания места ошибки хотя бы с точностью до функции, она указывается с точностью «где-то среди всех твоих исходников, ищи сам». Конечно, теоретики код не пишут, и ошибки им искать/исправлять не приходится - по-этому для них это не проблема.

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

Здесь проблема в том, что в хаскеле нету Any, а полимофрный аргумент в подстановке - общий. По-этому при вызове сужается тип аргумента. То есть:

> (: foo (Any -> Any))
> (define (foo x) x)
> 

теперь foo возвращает any, по-этому если мы попытаемся с ним что-то сделать (например сложить с чем-нибудь) то получим эррор, как и должны с другой стороны:

> (: foo (All (A) A -> A))
> (define (foo x) x)
> (+ 1 (foo 2))
- : Integer [more precisely: Positive-Index]
3
> 

не тайпчекается

А должен?

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

Нет, скобочки - это аппликация (есть же нульарные ф-я, с-но (x) - вызов нульарной ф-и х). Блок - (begin x ...) - если хочешь исполнить формы х поочередно, или если хочешь ввести лексический контекст, то (let () x ...)

можно в посмотреть плюсовый код где add(int, double) -> double, add(rational, float) -> double, add(int, int) -> int? =)

rational я заменил на double (лень библиотеку подключать). В остальном — вот:

$ cat test.cpp
#include <iostream>
using namespace std;

double add(int x, double y)
{
   cout << "int, double" << endl;
   return x + y;
}

double add(double x, float y)
{
   cout << "double, float" << endl;
   return x + y;
}

int add(int x, int y)
{
   cout << "int, int" << endl;
   return x + y;
}


int main()
{
   double x = add(1, 1.0);
   int y = add(1, 2);
   float z = 1.0;
   add(x, z);
}

$ ./a.out
int, double
int, int
double, float

можно в посмотреть плюсовый код где add(int, double) -> double, add(rational, float) -> double, add(int, int) -> int? =)

Обычная и вполне валидная перегрузка. Или ты о том, что это будет плохой, негодный код?

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

Мы сравниваем перегрузку в C++ и Хаскелле. Мне пока не получилось сделать, чтобы Km 2 + M 50 возвращало M 2050. В C++ без проблем

у x4da в джуйке отличный момент, срывающий покровы с системы типов хаскеля и хаскидебилов.

В ответ на «чем плохо писать аннотации у топлевел ф-й»: «тем, что при более сложных примерах проще написать и вставить тот тип, который выведется, чем выводить его в уме.». То есть человек хуячит код, не зная типов, и просто бездумно подставляет то, что ему выводит тайпчекер. Отлично, чо. Надежная система типов в действии.

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

Так сделай тайпкласс (Num a, Num b, Num c) => MyPlus a b c where +: a -> b -> c и дальше хуячь инстансы как душе угодно

Еще раз для особо одаренных - проблема состоит в том, что вместо указания места ошибки хотя бы с точностью до функции, она указывается с точностью «где-то среди всех твоих исходников, ищи сам».

Для особо одаренных, тайпчеккер тебе точно сказал где ошибка типизации в твоём коде. А писал бы код без warning-ов (top level entity missing type signature это warning) так и вообще бы эту проблему никогда не увидел - высосано из пальца в общем.

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

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

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

да, в haskell нету subtyping, а проблема - ли это вопрос другой, для лисперов, наверное проблема.

теперь твой пример в случае haskell:

Prelude> let f x = x
Prelude> :t f
f :: t -> t

Prelude| let f x = (x+1)
Prelude> :t f
f :: Num a => a -> a

по-этому если мы попытаемся с ним что-то сделать (например сложить с чем-нибудь) то получим эррор,

Prelude> :{
Prelude| let f :: a -> a
Prelude|     f x = x+1
Prelude| :}

<interactive>:14:12:
    No instance for (Num a) arising from a use of ‘+’
    Possible fix:
      add (Num a) to the context of the type signature for f :: a -> a
    In the expression: x + 1
    In an equation for ‘f’: f x = x + 1

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

Prelude> (1::Double) + f 0
2.0
Prelude> :t it
it :: Double

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

Для особо одаренных, тайпчеккер тебе точно сказал где ошибка типизации в твоём коде.

Ты чего такой непонятливый, а? Он указал ошибку там, только потому что так звезды сложились. Если написать инференс (корректный инференс) по-другому, он покажет ошибку В ДРУГОМ МЕСТЕ. Он показывает ошибку там, где алгоритм унификации встречает противоречие, в зависимости о того, КАК ИМЕННО проходила унификация, это противоречие может встретиться ГДЕ УГОДНО.

Чтобы ты понял - у тебя есть граф, в графе две вершины, между ними есть путь, тебе надо пройти по этому пути из вершины в вершину зарашивая каждую последующую вершину в цвет предыдущей. При этом первая вершина - белая, а вторая - черная. Момент, в котором тебе придется перекрасить вершину в другой цвет - ошибка. Вопрос - в какой вершине этот момент произойдет? Ответ - совершенно в любой вершине на пути, в зависимости от порядка их обхода.

Алсо, нам не нужно чтобы чекер искал ошибки в типизации. Надо чтобы чекер искал ошибки в программе. Именно это его предназначение.

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

Если ты будешь подтверждать свои теории конкретным кодом и его выхлопом, как мы с монком, то все в порядке. Какая разница кто задвигает? Главное - что задвигается. 2*2=4, даже если это скажет человеК, который не умеет считать, не так ли?

да, в haskell нету subtyping, а проблема - ли это вопрос другой, для лисперов, наверное проблема.

Еще раз - тот факт, что чекер не может указать ошибку даже с точностью до модуля (не гвооря о точности до функции) - это проблемА АБСОЛЮТНО ДЛЯ ВСХЕ КТО ПИШЕТ РЕАЛЬНЫЙ КОД. И именно для того, чтобы такая проблема возникала как можно реже, представь себе, те люди, которые реально пишут реальный код на хаскеле договорились все топ-левел функции аннотировать.

получили ошибку

Ошибку ты получил т.к. указал тип функции. Речь же шла о том случае, когда тип ф-и НЕ УКАЗАН. Racket в этом случае подставит any и будет ошибка. Хаскель в этом случае подставит а (потому что any нет) и код прекрасно будет работать.

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

Вопрос в том, что умеет переменная, о свойствах которой ничего не известно. В случае Racket ей устанавливается тип Any (то есть что угодно, а значит о ней ничего неизвестно - все соответствует семантике), а в хаскеле Any нет, по-этому ей устанавливается тип a, который реализует АБСОЛЮТНО ВСЕ ТАЙПКЛАССЫ. То есть там где в ракетке устанавливается наиболее общий тип, который никуда сунуть нельзя, в хаскеле устанавливается наиболее узкий тип, который можно сунуть КУДА УГОДНО.

Ты чего такой непонятливый, а? Он указал ошибку там, только потому что так звезды сложились.

я уже раз десять написал почему ошибка показалась там, в этом треде, что не только я не читаю что мне пишут? Да и type inference конкретно в этой ошибке совершенно ни при чем:

blah :: String -> String -> String
blah = const $ length

main :: IO ()
main = print $ show (blah "foo")

типы никакие не выводятся, а ошибка та же. КАК ЖЕ ТАК?!??!?!

Алсо, нам не нужно чтобы чекер искал ошибки в типизации. Надо чтобы чекер искал ошибки в программе. Именно это его предназначение.

да, я понимаю, а у меня ещё есть знакомый, очень любит динамические языки, потому, что берешь статически типизированный, скармливаешь ему описание ТЗ в .odt, а тайпчеккер не ищет ошибки.

Тайпчеккер должен искать ошибки типизации и именно эти он и занимается.

Ошибку ты получил т.к. указал тип функции.

Договаривай до конца, пожалуйста. Ошибку я получил, т.к. указал тип функции менее строгий, чем эта функция должна иметь. В ракекте, ровно тоже самое:

> (: f1 (Any -> Any))
> (define (f1 x) (+ 1 x))
stdin::133: Type Checker: type mismatch
  expected: Number
  given: Any

это ровно та же ошибка.

Речь же шла о том случае, когда тип ф-и НЕ УКАЗАН. Racket в этом случае подставит any и будет ошибка.

Хаскель в этом случае подставит а (потому что any нет) и код прекрасно будет работать.

Так.. меня это окончательно достало, давай ты по пунктам распишешь как работает typechecker и type inference в haskell, а то мне уже достало читать такие утверждения.

В ракетке, так же как и в haskell тип выводится на основе свойств, которые должна иметь переменная, так если мы складываем её с чем-то, то в ракетке выводится Num, а в haskell выводится 'Num a => a'. В haskell 'a' подставляется тогда и только тогда, когда на вход функции могут поступать _любые_значения_, соотвественно использующий ее код может подставлять туда что угодно и это будет корректно.

Например, в ракетке я легко могу написать код с типов Int -> Any, который будет возвращать что угодно. Написать такую хреноту в haskell не используя экзестенциальные типы.

MyPlus a b c where +: a -> b -> c

Не хотелось свой оператор делать, хотелось доопределить существующий. Кстати, а как проверить, например, что a типа Float? Пишу MyPlus (Float x) y z = ... --- ругается, что «нет такого конструктора».

типы никакие не выводятся, а ошибка та же

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

Предполагаю, что Haskell опять предложил поискать ошибку в show и доопределить инстанс.

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

А зачем ты это писал? Все и так прекрасно знали, почему она там. Разговор о том, что он показал ошибку не там, где она была.

типы никакие не выводятся, а ошибка та же. КАК ЖЕ ТАК?!??!?!

Здесь другая ошибка.

Тайпчеккер должен искать ошибки типизации и именно эти он и занимается.

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

Договаривай до конца, пожалуйста. Ошибку я получил, т.к. указал тип функции менее строгий, чем эта функция должна иметь. В ракекте, ровно тоже самое:

Нет, только потому, что ты тип УКАЗАЛ.

Нет, не то же самое. Вот различие:

(define (f x)
  x)

(+ 1 (f 1))

. Type Checker: type mismatch
  expected: Number
  given: Any in: (f 1)

Prelude> let f x = x
Prelude> 1 + f 1
2
Prelude>

Так.. меня это окончательно достало, давай ты по пунктам распишешь как работает typechecker и type inference в haskell, а то мне уже достало читать такие утверждения.

Тайпчекер - это и есть выводильщик типов. Работает он при помощи обычной унификации.

Таким образом ошибка должна быть «не хватает аргумента для blah».

Мы опять возвращаемся к тому, что привычки из других языков переносятся туда куда не следует. Учитывая, что все функции в haskell это функции от одного аргумента возвращающие другую функцию использование blah «s» это корректная функция возвращающая функцию с типом ":: String -> Int".

Предполагаю, что Haskell опять предложил поискать ошибку в show и доопределить инстанс.

опять за старое, будем учиться читать по слогам и понимать?

    No instance for (Show (String -> Int)) arising from a use of ‘show’
    In the second argument of ‘($)’, namely ‘show (blah "foo")’
    In the expression: print $ show (blah "foo")
    In an equation for ‘main’: main = print $ show (blah "foo")

Это значит, что т.к. ты используешь show, то у параметра должен присутсвовать инстанс Show, данная ошибка обозначает, что проблема в аргументе передаваемом show, а не в show.

Ты с концепцией интерфейсов знаком? В ракетке есть они? Просто видимо нужно на чем-то более доступном объяснять :/

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

Prelude> :set -XMultiParamTypeClasses
Prelude> class MyPlus a b c where (+:) :: a -> b -> c
Prelude> instance MyPlus Float Int Float where a +: b = a + fromIntegral b
Prelude GHC.Float> instance MyPlus Float Int Double where a +: b = float2Double  $ a +: b
Prelude GHC.Float> (2.0 :: Float) +: (1::Int)

<interactive>:10:1:
    No instance for (MyPlus Float Int a0) arising from a use of ‘it’
    The type variable ‘a0’ is ambiguous
    Note: there are several potential instances:
      instance MyPlus Float Int Double -- Defined at <interactive>:9:10
      instance MyPlus Float Int Float -- Defined at <interactive>:6:10
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it

Prelude GHC.Float> (2.0 :: Float) +: (1::Int) :: Double
3.0
Prelude GHC.Float> :t it
it :: Double

Кстати, а как проверить, например, что a типа Float?

может стоит учить язык последовательно? ;)

P.S. кстати 2 инстанса отличающиеся возвращаемым значением при одинаковых параметрах могут порадовать некоторые другие ЯП. Как я понимаю в ракетке про это и писали, почему отказались от тайпклассов (третья причина).