Прив. поможет кто дописать функцию? data N where S ::

Question

ǧ̥̹̤̪̉l̜̦̇̈͋a̮͕̭͙̗̓̓͑z̓̏ä͈̟͔́͌͌͋_̤̼̍p̙̘͙̮͑̓̔̃̄r͚͓̰͇ͫ͑̑͒a͕̬͈͋͊̽v

Прив. поможет кто дописать функцию? data N where S ::

N -> N
Z :: N

data V :: N -> * -> * where
Cons :: t -> V l t -> V (S l) t
Nil :: V Z t

type family a > b where
(S a) > (S b) = a > b
(S _) > Z = True
_ > _ = False

gbi :: l > i ~ True => V l t -> Proxy i -> t
gbi = undefined

r = gbi (Cons 1 (Cons 2 Nil)) (Proxy :: Proxy (S Z))
-- r == 2

вот она щас андефайнд а надо что была дефайнд. помогите плиз

#haskell #programming #russian

0

31.07.2021

5 ответов

8 просмотров

ǧ̥̹̤̪̉l̜̦̇̈͋a̮͕̭͙̗̓̓͑z̓̏ä͈̟͔́͌͌͋_̤̼̍p̙̘͙̮͑̓̔̃̄r͚͓̰͇ͫ͑̑͒a͕̬͈͋͊̽v Автор вопроса

Zygohistomorphic Prepromorphism🇺🇦
а зачем прокси? если через финит можно data Fin n...

хотел через констрейнты чтобы не делать лишнее vhead :: l > Z ~ True => V l t -> t vhead (Cons v _) = v так получилось, думал что и с gbi можно будет

0

31.07.2021

Cheese Syrowiecki

домашняя работа?

0

31.07.2021

TOV_MULTIMASSO

Сделай > классом, и чтобы оно предоставляло type-level N

0

01.08.2021

ǧ̥̹̤̪̉l̜̦̇̈͋a̮͕̭͙̗̓̓͑z̓̏ä͈̟͔́͌͌͋_̤̼̍p̙̘͙̮͑̓̔̃̄r͚͓̰͇ͫ͑̑͒a͕̬͈͋͊̽v Автор вопроса

TOV_MULTIMASSO
Сделай > классом, и чтобы оно предоставляло type-l...

Не понял. Объясни примером пожалуйста

0

02.08.2021

Zygohistomorphic Prepromorphism🇺🇦 · Accepted Answer

Zygohistomorphic Prepromorphism🇺🇦

а зачем прокси? если через финит можно data Fin n where FZ :: Fin (S n) FS :: Fin n -> Fin (S n) gbi :: V l t -> Fin l -> t gbi (Cons x _) FZ = x gbi (Cons _ xs) (FS n) = gbi xs n

0

31.07.2021

169 похожих чатов

Прив. поможет кто дописать функцию? data N where S ::

5 ответов

Похожие вопросы