что-то знакомое, емнип бложек про околофп

Романа Душкин вел блог в ЖЖ с таким названием

oh

можно его на Facebook или в твиттере спросить он там активен

@bravit111 может ты знаешь?

Спасибо большое всем, кто сегодня принимал участие в процессе написания моего парсера!

Вы очень здорово помогли

и где конечный результат?)

а как в Хаскеле теоремы про type level функции доказывать?

unsafeCoerce

:D

вот есть type family RecTy (l :: Symbol) (lts :: [k1]) :: k where RecTy l (l := t ': lts) = t RecTy q (l := t ': lts) = RecTy q lts

все что примитивными TF не покажется не сработает

и type family DB' (schema :: [(Symbol, [*])]) where DB' '[] = '[] DB' ('(l, r) ': fs) = l := [Rec r] ': DB' fs

хочу из RecTy t schema r уметь получать RecTy t (DB' schema) [Rec r]

вроде кажется просто...

unsafeCoerce как-то не очень... но для прототипа сойдет, наверное

не понимаю, RecTy это функция, получить из результат применения функции результат другой функции?

да, я написал, как будто это констрейнт, сорри

хочу RecTy t schema ~ RecTy t (DB' schema), конечно

хочу RecTy t schema ~ RecTy t (DB' schema), конечно

тут хватит доказать что schema ~ DB' schema? или нет

так они не равны, зачем бы иначе огород городить?

schema -- это список пар (Symbol, Row), а DB' schema -- это список пар (Symbol, [Rec r])

Row ~ [Rec r]? насколько я помню то рекорд изоморфен списку пар вроде

тайплевел списку

это да

но DB' берет Row и возвращает тип списка рекордов с этим Row

ok, тут unsafeCoerce помог, а как мне констрейнты коерсить?

как бы мне постулировать RecSize schema ~ RecSize (DB' schema)?

как бы мне постулировать RecSize schema ~ RecSize (DB' schema)?

не знаю, мб как-то заюзать https://www.stackage.org/haddock/lts-11.15/constraints-0.10/Data-Constraint.html#t:Dict

но я не знаю точно

@bravit111 может ты знаешь?

Не, не в курсе

хм. Как-то я им пользовался, там вылезают ошибки типа, которые без Эдварда не понятно, как фиксить 🙂 попробую еще раз

хм. Как-то я им пользовался, там вылезают ошибки типа, которые без Эдварда не понятно, как фиксить 🙂 попробую еще раз

у него есть пару постов http://comonad.com/reader/2011/what-constraints-entail-part-1/ http://comonad.com/reader/2011/what-constraints-entail-part-2/

да он и отвечает на #haskell, на это вся и надежда 🙂

хочу RecTy t schema ~ RecTy t (DB' schema), конечно

через класс типов

или TF a b возвращающую Refl a b

а не класс типов, да, то ещё удовольствие в Haskell

Получился обычный парсер. Вечером оказалось, что конечный вид меседжей еще не утвержден, так что сам конструктор я пока писать не буду:)

и где конечный результат?)

Или вам интересен сам код?

Да, можем поревьюить :)

меня продолжает кусать та же ошибка с переименованием:

recSizeOfDB :: forall schema. RecSize (DB' schema) :~: RecSize schema

• Couldn't match type ‘RecSize (DB' schema0)’ with ‘RecSize (DB' schema)’ Expected type: RecSize (DB' schema) :~: RecSize schema Actual type: RecSize (DB' schema0) :~: RecSize schema0

ScopedTypeVariables + forall schema?

и дальше про то, что RecSize is a type function, and may not be injective

ну

но я это знаю, я как раз хочу теорему, что есть равенство 🙂

ScopedTypeVariables включил

и schema в forall?

forall есть

а можно гист?

у меня наконец-то телеграм на компе есть

можно github: https://github.com/yanok/queLam/blob/master/src/QueLam/R.hs

src/QueLam/Core.hs:44:17: error: Not in scope: type constructor or class ‘RecVecIdxPos’ | 44 | , KnownNat (RecVecIdxPos l sortedFlds)

Да, там надо патченый superrecord

Стеком должно собираться сорри 😀

у меня new-build-ом нормально

так как теперь заставить его сломаться?

чтобы увидеть проблему

@ilya_yanok ^

Хм

блин, сорри, я не закомитил

хм, нет, вроде закомитил

@qnikst у тебя QueLam/R.hs собирается?

7a22bb269b2ce5bf3615a19b77ba5301354a61a1 <- ?

а может не добавлен в cabal

точно у тебя ж hpack

угу, это все стэк 🙂

скорее hpack

стек-то ещё куда ни шло

стэк сейчас hpack по умолчанию предлагает

всегда знал что стек это плохо

блин на ноуте опять сдох телеграм и чтож такое

Это было бы замечательно:)

Да, можем поревьюить :)

Завтра скину

я заставил ту штуку скомпиляться

не ясно что с суперрекордом делать, который неиндуктивный нифига