Не могли ли бы вы подсказать врзможно ли както class Contextual

Question

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

Не могли ли бы вы подсказать врзможно ли както class Contextual

(container :: * -> [*] -> *)
class (∀a b (t :: a -> b -> *). Contextual t, Contains Fresh b ~ True)
=> Canonnical t

почему жшс орёт что б не в скоупе? и можно ли обращаться к [*]?

#haskell #programming #russian

0

31.03.2021

3 ответов

9 просмотров

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

Lierdakil
В общем я подумал немного и по-моему так совсем не...

Любой, который содержит тип фрэш.

0

31.03.2021

Lierdakil

ǧ̥̹̤̪̉l̜̦̇̈͋a̮͕̭͙̗̓̓͑z̓̏ä͈̟͔́͌͌͋_̤̼̍p̙̘͙̮͑̓̔̃̄r͚͓̰͇ͫ͑̑͒a͕̬͈͋͊̽v
Любой, который содержит тип фрэш.

По kind-сигнатуре вообще любой. Ограничить kind-сигнатурой типы в списке нельзя, это уже какие-то dependent kinds получаются

0

31.03.2021

Lierdakil · Accepted Answer

В общем я подумал немного и по-моему так совсем нельзя. Что b не определено это понятно, если записать ∀a b (t :: a -> b -> *). Contains Fresh b ~ True => Contextual t то b в скоупе. А то там же кортеж, а forall связывается с элементом кортежа. Но всё равно не получится, потому что b не kind, и DataKinds не промоутятся. Поэтому сослаться на b :: [*] в kind-сигнатуре уже нельзя. Более того, если b :: [*], то значит b ~ '[x, y, z, ...]. Но это довольно абсурдный kind даже если бы он промоутился! b :: [*] не значит что b ~ [*]. Я так понимаю идея в том чтобы привязаться к конкретному typelevel списку. Так это сделать не получится, у container никакого списка ещё нет, он его только ждёт. И ведь любой подойдёт ему.

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

Не могли ли бы вы подсказать врзможно ли както class Contextual

3 ответов

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