Описание тега free-theorem

Вопросы с тегом
Инструмент для генерации бесплатных теорем для подъязыков Haskell.
1 ответ

Для различных возможных экземпляров Monad типа всегда подразумевается экземпляр Functor?

Согласно Typeclassopedia и этой ссылке тип может иметь только один Functor экземпляр (есть ссылка в ссылке). Но я понимаю, что для данного типа возможно иметь несколько возможных Monad случаи, это правильно? Но для данного Monad экземпляр есть беспл…
13 фев '14 в 17:28
1 ответ

Нахождение "свободной теоремы"

Как вывести свободную теорему для типа: data F a = C1 Nat | C2 Bool Nat a где Nat это просто data Nat = Z | S Nat? В принципе, на это может ответить пакет "свободных теорем" на Haskell, но он слишком стар для компиляции под любой версией GHC, котору…
17 ноя '18 в 13:58
1 ответ

В Идрисе я могу доказать свободные теоремы, например, единственную (полную) функцию типа `forall t. t -> t` это `id`?

Для достаточно полиморфных типов параметричность может однозначно определять саму функцию (подробности см. В теоремах Вадлера бесплатно! ). Например, единственная общая функция с типом forall t. t -> t это тождественная функция id, Можно ли утвер…
27 май '17 в 06:11
1 ответ

Параметрические доказательства в Агде

Чтение этого ответа побудило меня попытаться построить, а затем доказать каноническую форму полиморфных контейнерных функций. Конструкция была простой, но доказательство ставит меня в тупик. Ниже приведена упрощенная версия того, как я пытался напис…
21 дек '15 в 03:20
1 ответ

Paramcoq: свободные теоремы в Coq

Как я могу доказать следующую бесплатную теорему с плагином Paramcoq? Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X), f X x = x. Если это невозможно, то какова цель этого плагина?
11 мар '19 в 22:46
2 ответа

Закон для типа [[a]] -> ([a], [a])

Я пытаюсь ответить на этот вопрос из своей домашней работы: Учитывая произвольный foo :: [[a]] -> ([a], [a]), запишите один закон, что функция foo удовлетворяет, включая map по спискам и парам. Некоторый контекст: я учусь на первом курсе курса фу…
15 дек '19 в 23:51
2 ответа

Тривиален ли закон распределения функторов для класса типов ʻAlt`?

Я смотрел на законы о Alttypeclass, который выглядит так: class Functor f => Alt f where (<!>) :: f a -> f a -> f a Один из законов звучит так: <$> left-distributes over <!>: f <$> (a <!> b) = (f <$> a) &…
24 фев '20 в 20:50
1 ответ

Бесплатная теорема для fmap

Рассмотрим следующую оболочку: newtype F a = Wrap { unwrap :: Int } Я хочу опровергнуть (в качестве упражнения, чтобы осмыслить этот интересный пост ), что существует законный Functor F экземпляр, который позволяет нам применять функции Int -> In…
24 апр '21 в 22:16