Телеграмм чат группы haskellru страница 16602

17:25пожаловаться #1

А так опять нет

baz :: (forall r . (forall n . KnownNat n => Proxy n -> r) -> r) -> String
baz f = f \(Proxy :: Proxy n) -> x @n

Это точно так должно быть?

17:26пожаловаться #2

что-то с имплисит импортом Data.Type.Bool не завелось (не находит)
щас поищу, откуда оно

17:27пожаловаться #3

Maxim Koltsov in Haskell

Data.Type.Equality

17:28пожаловаться #4

да

17:28пожаловаться #5

Maxim Koltsov in Haskell

вечно путаю

17:28пожаловаться #6

все еще duplicated instance declaration

17:28пожаловаться #7

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

17:29пожаловаться #8

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

17:29пожаловаться #9

Да, вопрос-то почему работает это

bar :: SomeNat -> String
bar (SomeNat (Proxy :: Proxy n)) = x @n

При том что такое ожидаемо не работает

baz :: (forall r . (forall n . KnownNat n => Proxy n -> r) -> r) -> String
baz f = f \(Proxy :: Proxy n) -> x @n

17:31пожаловаться #10

Чтобы сделать то что ты тут хочешь надо name ~ “” вынести в голову (после `=>`). Читать тут: https://kseo.github.io/posts/2017-02-05-avoid-overlapping-instances-with-closed-type-families.html

17:31пожаловаться #11

А инстансы там какие?

17:31пожаловаться #12

спасибо, щас прочту

17:32пожаловаться #13


instance {-# OVERLAPPING #-} Foo 0 where
  x = "zero"

instance {-# OVERLAPPABLE #-} (KnownNat n) => Foo n where
  x = show $ natVal $ Proxy @n

17:32пожаловаться #14

Похоже, да. Пойду на всякий случай доку OVERLAPPING перечитаю

17:33пожаловаться #15

Мне кажется, он всегда будет выводить число, даже есть передать 0

17:33пожаловаться #16

В плане zero не будет выводить

17:33пожаловаться #17

Если будет, то я очень сильно удивлюсь

17:33пожаловаться #18

Но это не отвечает на вопрос, почему одно работает, а другое нет

17:34пожаловаться #19

Overlapping instances в этом плане очень странный и его нужно пытаться избегать когда возможно