Replies (19)

  • @qnikst, ну дак да, где доказательство-то
  • @rkit, эм.. а куда тут дальше доказывать?
  • @qnikst, да самом деле тупо недоработка, которую наверное никогда не пофиксят ибо:

    Comparison of type-level naturals, as a function. NOTE: The functionality for this function should be subsumed by CmpNat, so this might go away in the future. Please let us know, if you encounter discrepancies between the two.
    а эту связь руками вразумительным образом я так понимаю не доказать
  • @qnikst, в haskell а не нормальном ЯП
  • @qnikst, Связь между функциями CmpNat и <=?
    Ты надеешься, что комплятор сам догадается, что они одинаковые?
  • @rkit, естественно эта связь должна уже быть доказана в base, где CmpNat и <=? определены, возможно с поддержкой на стороне компилятора, как обучили typelevel арифметике, в районе 7.10.
  • @qnikst, Ну как ты правильно заметил, в хаскеле ее доказать. А компилятор кошмарить хардкодом всех возможных комбинаций — это бред.
  • @rkit, для вещей с очевидной связью написаных в одном модуле, с некоторой долей очевидности эта связь должна существовать и поддерживаться компилятором. Ты мне ещё тут про то, что для KnownNats n+m == m+n я сам должен доказывать порассказывай :)
  • @qnikst, ты должен прекратить ожидать, что это так в хаскеле
  • @qnikst, в каком-нибудь coq шаг в сторону и миллионы таких кошмаров
  • @rufuse, доказывается пусть и прямолинейно для таких случаев, но для программиста — жесть полная
  • @rufuse, очень дотошно все это делать, т.е.
  • @rufuse, ну тут как сделать доказательство я знаю, но при этом потеряются все бонусы, т.к. придётся делать uni-nats и синглетоны, а приколько было бы использовать Typelevel Naturals
  • @qnikst, мне вот тоже казалось что это требует перепиливания в GHC, потому что если хочешь сделать какие-нибудь рациональные/вещественные числа на тайплевеле, тоже хочется нормальные литералы
  • @rufuse, ну рациональные и вещественные сделать то можно, но на больше, чем проверку равенства рассчитывать врятли придётся
  • @qnikst, я вообще не сильно понимаю, как можно что-то интересное без стратегий запиливать, или придётся какой-то ад с кучей wrapper типов делать
  • @qnikst, агда как раз для исследования этого вопроса кмк
  • @rufuse, я "стратегии" как "тактики" прочитал. Ты что-то другое в виду имел или я правильно понял?
  • @rufuse, да их.