Я понимаю.

data Equality a b where
    R :: Equality a a

leftPlusZeroIsId :: SNat n -> Equality (Add Zero n) n
leftPlusZeroIsId _ = R

Задача: сделать такую же штуку для умножения на ноль слева. Делаю:

leftProdZeroisZero :: SNat n -> Equality (Product Zero n) Zero
leftProdZeroisZero _ = R

правильно?.. Тайпчек проходит.

идея в чем, Product Zero n может быть вычислен тайпчекером, потому что функция Product матчит по первому аргументу, и первый аргумент тут в явном виде - Zero
поэтому Product Zero n и Zero равны по определению Product, поэтому тайпчекеру это ок для того чтобы просто использовать Refl, который требует чтобы значение слева и справа были равны

а вот например с (Product n Zero) :~: Zero так уже не выйдет, Product n Zero нельзя вычислить не зная n, поэтому тут нужно уже доказывать по индукции, в коде через рекурсию

data N = Z | S N

data SN n where
 SZ :: SN Z
 SS :: SN n -> SN (S n)

type family n + m where
 Z + m = m
 S n + m = S (n + m)

congr :: forall f a b. a :~: b -> f a :~: f b
congr Refl = Refl

plus_left_id :: SN n -> Z + n :~: n
plus_left_id _ = Refl

plus_right_id :: SN n -> n + Z :~: n
plus_right_id SZ = Refl
plus_right_id (SS n) = congr @S (plus_right_id n)

о, я смотрю кто-то таки стал решать лабу

Где можно почитать?.. Вот например задача:

type IntSet = (Int -> Bool)
isMember :: IntSet -> Int -> Bool
isMember f x = f x

emptySet :: IntSet
emptySet x = ...
allInts :: IntSet
allInts x = ...

Я стал.

а че за лаба

Аргонная :).

кажется мне эта статья не понравилась

Ещё есть какие-то книги?.. В моей четвёрке ничего об этом нет и не гуглится.

ну, я там не понял, как произошел плавный переход из k -> Maybe v в k -> v

На канале твига Айзенберг как раз про это рассказывает

о чем, о вот этих Equality? Тут нужно читать про type families, gadt, coercions

Ага, благодарю.

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

Это тот, что лабы людям делает?

Не тот, а я!

Я кое-как написал такую вот жуткую функцию:

setByte :: forall (ix :: Nat) (width :: Nat). (9 <= width, ix + 1 <= width `Div` 8, KnownNat ix, KnownNat width) => NatRepr ix -> BV 8 -> BV width -> BV width
setByte ix val bv = Data.BitVector.Sized.or bv shifted
    where extendedVal = zext (knownNat @width) val
                shifted = shl (knownNat @width) extendedVal $ natVal (Proxy @ix) * 8

И у меня конпелятор ругается что первый аргумент (ix) - не используется.
В доке к NatRepr написано, что это A runtime presentation of a type-level Nat..
В теле функции ix как значение тоже не используется, насколько я понимаю, т.е. runtime presentation здесь действительно не нужен.
Одна если я просто уберу этот аргумент, то ругается could not deduce KnownNat ix0
Кто-нибудь может объяснить как можно убрать NatRepr ix из аргументов или я ошибаюсь в его ненужности?