Публикации по теме 'type-theory'
Поручение ДУРАКА: давайте создадим настоящий язык FP с нуля (на Haskell)
Применение FP и теории типов на практике
Поручение ДУРАКА: давайте создадим настоящий язык FP с нуля (на Haskell)
Часть 1: Введение — почему; ранняя архитектура компилятора; Nat, Bool, суммирование, равенство; Введение в «Машину основных списков»
Это первая статья из серии, описывающей создание FOOL3: функциональный объектно-ориентированный язык низкого уровня — язык функционального программирования с мощной системой типов (настолько близкой к Исчислению конструкций , насколько..
Вопросы по теме 'type-theory'
может ли кто-нибудь объяснить связь между ковариантностью/контравариантностью типов и теорией категорий?
Я только начинаю читать о теории категорий и был бы очень признателен, если бы кто-нибудь мог объяснить связь между контравариантностью/ковариантностью CS и теорией категорий. Какими могут быть некоторые примеры категорий (т.е. каковы их...
749 просмотров
schedule
08.12.2023
Вид против ранга в теории типов
Мне трудно понять типы Higher Kind vs Higher Rank. Вид довольно прост (спасибо за это литературе по Haskell), и я раньше думал, что ранг похож на вид, когда речь идет о типах, но, по-видимому, это не так! Я прочитал статью в Википедии...
1645 просмотров
schedule
31.08.2023
Саморепрезентация и вселенные в ОТТ
Вопрос касается теории наблюдательных типов .
Рассмотрим этот параметр:
data level : Set where
# : ℕ -> level
ω : level
_⊔_ : level -> level -> level
# α ⊔ # β = # (α ⊔ℕ β)
_ ⊔ _ = ω
_⊔ᵢ_ : level -> level -> level
α ⊔ᵢ...
187 просмотров
schedule
20.06.2022
Мира мало
Я все еще пытаюсь внедрить теорию типов наблюдений в себя и все это в Агду.
В настоящее время у меня есть следующая иерархия вселенных:
Prop : Type 0 : Type 1 : ...
(∀ α -> Type α) : Type ω₀ : Type ω₁
Чтобы определить равенство...
208 просмотров
schedule
10.06.2023
Как сопоставить с образцом на опоре при испытании в Coq без исключения на Type
Я пытаюсь доказать, что хвост отсортированного списка сортируется в Coq, используя сопоставление с образцом вместо тактики:
Require Import Coq.Sorting.Sorted.
Definition tail_also_sorted {A : Prop} {R : relation A} {h : A} {t : list A}...
514 просмотров
schedule
04.05.2022
Поиск наиболее общего унификатора в Haskell с использованием Data.Comp.Unification (вопрос для начинающих)
У меня есть следующая структура в haskell, которая реализует некоторые механизмы для печати и вызывает унификатор. Я получаю следующую ошибку от main:
0 =/= int
Кажется, что 0 - это число, а не переменная. Ниже приведена полная реализация....
351 просмотров
schedule
05.12.2023
Объединение типов более высокого ранга на контравариантных позициях
Быстрый пример:
{-# LANGUAGE RankNTypes #-}
l :: (forall b. [b] -> [b]) -> Int
l f = 3
l1 :: forall a. a -> a...
75 просмотров
schedule
27.01.2024
Интуиционистская пропозициональная логика
Я изучал интуиционистскую логику и то, что называется отрицательным фрагментом интуиционистской пропозициональной логики. Однако мне не удалось найти ни одного ресурса, объясняющего причину, по которой он называется отрицательным фрагментом.
Любые...
42 просмотров
schedule
16.02.2023
API для стратегий доказательства теорем
Существуют ли высокоуровневые API/среды/библиотеки для проверки эффективности конкретного подхода (например, эвристического алгоритма) для создания конструктивных доказательств на основе логики первого порядка/теории типов?
Я пытаюсь найти удобный...
122 просмотров
schedule
30.11.2022
Что такое грамматика System FC2 для видов?
Я пытаюсь понять этот пост в блоге о расширении ConstraintKinds .
В разделе комментариев был пост, который я совершенно не понял. Вот:
Адам М говорит: 14 сентября 2011 г., 19:53 UTC
Вау, это звучит здорово. Планируется ли он стать...
92 просмотров
schedule
28.10.2023
