Type family RecurseAndCheck a b where RecurseAndCheck a

Question

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

Type family RecurseAndCheck a b where RecurseAndCheck a

(HList '[]) = CSat
RecurseAndCheck a (HList ((l :: a) : b)) = RecurseAndCheck a (HList b)
RecurseAndCheck a (HList ((k :: r) : b)) = CNSat
class (forall t (a :: HList t) . RecurseAndCheck (Pair Symbol *) a)
=> Record a

можно это заставить работать?

#haskell #programming #russian

0

23.03.2021

3 ответов

5 просмотров

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

Хочу сказать "любой хлист элементы которого принадлежат роду (Symbol, *) это рекорд". Как?

0

23.03.2021

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

aadaa_ftgaa
Вы же вроде справшивали про это в багтрекере ghc, ...

А сделать общую версию Check возможно? Не хочется писать под каждый кейс. И ещё смежный вопросик - почему стринги не лифтятся автоматом, как это делают числа ?

0

23.03.2021

aadaa_ftgaa · Accepted Answer

Вы же вроде справшивали про это в багтрекере ghc, вам там правильно сказали что элементы хлиста всегда кайнда Type, a (Symbol, Type) /= Type. Так что проверять что элементы хлиста имеют кайнд (Symbol, Type) бессмысленно - точно не имеют. Чтобы сделать рекорд на хлистe вы можете объявить ньютайп newtype Field (name :: Symbol) typ = Field typ и считать рекордом такой хлист, у которого все типы элементов вида Field _ _ (кайнда Type) . Проверять тогда можно как-то так: type family Check ts where Check (HList '[]) = () :: Constraint Check (HList (Field _ _:r)) = Check (HList r) Check (HList (t:_)) = TypeError ('Text "Non-Field type in record: " ':<>: 'ShowType t) class Check ts => Record ts instance Check ts => Record ts Но лучше конечно сделать как Adam Gundry написал, что-нибудь типа data Record ts where RNil :: Record '[] (:>) :: x -> Record xs -> Record ('(name, x) : xs) Тогда у вас Record является рекордом by construction, никаких проверок не нужно. См. parse, not validate. Или, если вы все-таки хотите сделать на хлисте, например чтобы рекорд можно было использовать как хлист, можно взять более общий хлист параметризованный типом f: -- Data.SOP.NP из sop-core, NP Identity ~= HList data NP f xs where Nil :: NP f '[] (:*) :: f x -> NP f xs -> NP f (x:xs) infixr 5 :* type Snd :: (a, b) -> b type family Snd t where Snd '(_, b) = b newtype Field nt = Field (Snd nt) type Record = NP Field foo :: Record [ '("foo", Bool), '("bar", Int) ] foo = Field True :* Field 1 :* Nil

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

Type family RecurseAndCheck a b where RecurseAndCheck a

3 ответов

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