Обновление n-арного продукта из sop-core на совместимую сумму

Я работаю с библиотекой sop-core и хочу написать функцию со следующим типом:

patch :: NS I xs -> NP Maybe xs -> NP Maybe xs

xs - это список типов на уровне типа, например '[Int,Char,Bool]. I - это функтор тождества. NS I xs - это тип n-арной суммы. NP Maybe xs - это n-арный продукт, в котором каждый компонент может существовать, а может и не существовать.

patch должен взять значение из n-арной суммы и заполнить соответствующий слот n-арного продукта, перезаписав его, если он уже существует. Например:

patched :: NP Maybe '[Int,Char,Bool]
patched = patch (Z (I 3)) (Nothing :* Nothing :* Nothing :* Nil)
-- patched == Just 3 :* Nothing :* Nothing :* Nil

Я подозреваю, что решение может включать injections, но я в тупике.


haskell type-level-computation algebraic-data-types
person danidiaz    schedule 26.10.2019    source источник
comment
Возможно связано: stackoverflow.com/questions/53692296/   -  person danidiaz    schedule 26.10.2019

Ответы (1)


arrow_upward
2
arrow_downward

Для решения не требовалось injections в конце концов, но _ 2_, которая преобразует сумму в продукт, заполняя несовпадающие компоненты продукта значением по умолчанию.

Уловка состоит в том, чтобы создать продукт из сеттеров, который мы можем применить к исходной записи, используя _ 3_. Когда мы расширяем сумму, несовпадающие компоненты заполняются функцией идентичности. Но мы перезаписываем совпадающий компонент значением суммы.

Для начала нам понадобится этот вспомогательный тип

newtype Mendo a = Mendo { getMendo :: Maybe a -> Maybe a }

а код для patch будет:

patch :: forall xs. SListI xs => NS I xs -> NP Maybe xs -> NP Maybe xs
patch piece =
  let mendos :: NP Mendo xs -- product of setters
      mendos = expand_NS (Mendo id) (liftA_NS (\(I x) -> Mendo (\_ -> Just x)) piece)
   in liftA2_NP (\(Mendo f) x -> f x) mendos
person danidiaz    schedule 26.10.2019