• ? Haskell typefun Вот есть у меня, например, Proxy (n::Nat), можно как-нибудь убедить компилятор, что оно удовлетворяет какому-нибудь ограничению, типа

    data P where
    P :: (n < 255) => Proxy n -> P

    magick :: Proxy n -> Maybe P
    magick = undefined


    даже unsafeCoerce не спасает..

Replies (18)

  • @qnikst, если получится, то в P :: KnownNat n ещё пихнуть.
  • @qnikst, Где ты взял <? С <= вот этот код собрался
  • @rkit, <=
  • @rkit, Так ну и magick :: SomeNat -> Maybe P
    Т.к. с Proxy нужно просто констрейнт добавить
  • @qnikst, Да тоже собралось
  • @rkit, С чем-то осмысленным вместо undefined?! КаК?
  • @rkit, Напр. magick = Just.P // да я знаю что это не агда
  • @qnikst, Без андефинед, естественно.
  • @rkit, Как?!
  • @qnikst, С андефинед. Что-то я туплю с голода сильно.
  • @rkit, Единственное, что можно попробовать, это написать класс, который индуктивно сравнивает наты.
  • @rkit, Прикольно
  • @qnikst, типа (n < 255) не работает?
  • @Shchvova, Да у тебя есть n — которое любой Nat, и компилятор не может вывести, что n < 255, а "обмануть" его и подставить неясно как (ну точнее @rkit привёл вариант) ещё можно для bounded через sameNat все перебрать. // ещё можно доказательство через тег попробовать потасать// но и то и другое в жизни нафиг не нужно
  • @qnikst, Есть тип n :: Nat.
    Есть класс ToInteger n where toInteger :: Proxy n -> Integer
    Компилятор не верит тому, что если toInteger (x :: Proxy n) < 255, то и n < 255.
    Вообще то что я предложил тоже не поможет. Только зависимые типы.
  • @rkit, Хотя опять вру, класс поможет. С ним можно вообще без рантайма обойтись.
  • @rkit, Не очень понимаю как можно обойтись без рантайма, если значение будет известно только в рантайме..
  • @rkit, в общем получилось что-то похожее на решение с перебором (сделано через closed TypeFamily и [Nat]), и классом. Жуть полная..