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

Скаланы need help. Дано Базовый тип: sealed trait Op[A], Наследники Op: OpX1,

OpX2 ... OpXn вида case class OpXn(...) extends Op[Xn]
Нужно доказать что имея инстанс типа
(OpX1 => F[X1]) :: (OpX2 => F[X2]) :: ... :: OpXn => F[Xn] :: HNil
для любого F[_]: Functor я могу получить инстанс Op ~> F.

Я смог получить промежуточную функцию
f: Generic[Op[_]]#Repr => F[X1 :+: X2 :+: ... :+: Xn :+: CNil]
и тогда
new (Op ~> F) {
def apply[A](op: Op[A]): F[A] =
f(Generic[Op[_]].to(op)).map(Coproduct.unsafeGet).asInstanceOf[F[A]]
}
И оно работает, и промежуточная функция точно верна и asInstanceOf[F[A]] безопасен,
но интересно можно ли подругому?

1 ответов

9 просмотров

Пока не складывается. По-видимости нет конструктивной индукции (forall x: Op[_]. exists i .x.type~ Op[Ci]), полагаю, в случае даже одного Op а это было бы эквивалентно аксиоме исключённого третьего, которой в явном виде нет в теории типов

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

Обсуждают сегодня

Мужики и девушки, привет) в Вelphi xe7 в настройках во вкладке "Editor Options" далее " Color" есть список: "Elements", открыв который мы можем настраивать отображение разных...
Kraszx
14
Добрый вечер. Есть вопрос, а может и предложение. Был у меня диалог в другой группе о делфи и я задался вопросом: "А нельзя ли в делфи цвет //коментария и {комментария} сде...
Kraszx
24
Всем привет! Подскажи, пожалуйста, как передать в TComboBox сразу значение и id записи. На Delphi я делал так: ComboBox1.Items.AddObject('Какое-то значение', Pointer(id запис...
Евгений
13
А вот это что за конструкция? Вернее, она тут нафига?
Serjone
10
Мдя, прикол, боевая сборка запускается (именно под отладчиком) после F9 примерно полторы минуты (97 секунд если быть точным). Начал копать - проблема детектится сразу - зависа...
Александр (Rouse_) Багель
38
Мужики. привет) в Вelphi xe7 в настройках во вкладке "Editor Options" далее " Color" есть список: "Elements", открыв который мы можем настраивать отображение разных элементов...
Kraszx
2
Здравствуйте, вопрос по структурам данных. Были у вас случаи, когда пришлось писать деревья или двунаправленные списки?
/ /
50
Товарищи, кто работа с iphelper? Или может я в самой логике ошибки фигачу, не пойму.... var ifTable : PMIB_IFTABLE; size, corSize: DWORD; Buffer ...
Warfarellen
4
я так понимаю, я так подозреваю, что создание такого плагина для человека, кто умеет писать плагины для делфи потребует минут 5-10 времени. но это мое подозрение. хотелось бы ...
Kraszx
7
Всем привет! Кто пользуется DevExpress, подскажите пожалуйста, реализован ли в TcxGrid в новых версиях поиск по датам как в Экселе (ну т.е. не просто список чекбоксов со значе...
A Z
4
Карта сайта