?

Log in

No account? Create an account
Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

coq-загадка [Jul. 6th, 2010|11:24 pm]
Программирование с зависимыми типами

zelych
А вот если выразить логические связки в таком виде:

Definition and (p q : Prop) := forall a : Prop, (p -> q -> a) -> a.
Definition or (p q : Prop) := forall a : Prop, (p -> a) -> (q -> a) -> a.

то для них, наверное, можно доказать какие-нибудь простые свойства:

Lemma or_distr : forall p q r, or p (and q r) -> and (or p q) (or p r).
Lemma or_assoc : forall p q r, or (or p q) r -> or p (or q r).

Только у меня почему-то, хоть убей, не получается.

Думал на хаскеле будет привычнее, перевёл or_assoc на него -- тоже не решается:

{-# LANGUAGE RankNTypes #-}

type OR p q = (forall a. (p -> a) -> (q -> a) -> a)

or_assoc :: OR (OR p q) r -> OR p (OR q r)
or_assoc h1 h2 h3 = undefined

h1 :: OR (OR p q) r -- ((forall b . (p -> b) -> (q -> b) -> b) -> a) -> (r -> a) -> a
h1 or_pq ra = undefined

h2 :: p -> a
h2 = undefined

h3 :: OR q r -> a
h3 or_qr = undefined


Отгадка для or_distrRead more...Collapse )
Отгадка для or_assocRead more...Collapse )
Подскажите что-нибудь, пожалуйста.
Link14 comments|Leave a comment

She. [Apr. 3rd, 2010|07:09 pm]
Программирование с зависимыми типами

thesz
[Tags|, ]

She is the Strathclyde Haskell Enhancement.

Препроцессор, добавляющий в Хаскель полезные вещи из области зависимых типов. Например, типы, индексированные данными.

Написан Конором МакБрайдом на его пути к Эпиграмму.

Узнал об этом через PFP Planet, из записи nealar.
Link2 comments|Leave a comment

Окончательная версия Coq 8.2 [Feb. 15th, 2009|12:30 am]
Программирование с зависимыми типами

alexey_rom
[Tags|]

Сабж вышел.
Link5 comments|Leave a comment

observational type theory [Feb. 9th, 2009|07:48 pm]
Программирование с зависимыми типами

beroal
Кто-нибудь раскусил, что такое «observational type theory» и с чем её едят? (См. пример задачи ниже.) Иль её не едят, ею любуются? ;) P. S. Статьи просматривал, голова всё равно осталась пустой.

Например, нужно записать высказывание «у морфизма m:a→b есть прообраз по функтору F». Должно получиться ∃a0.F a0 = a → ∃b0.F b0 = b → ∃m0:a0→b0.F m0 = m. Проблема в том, что в равенстве F m0 = m правая и левая части имеют разные типы, а именно: F m0:F a0→F b0 и m:a→b. Чтобы приравнять типы, надо применить равенства F a0 = a и F b0 = b.
Link11 comments|Leave a comment

Вышел Release Candidate Coq 8.2 [Jan. 25th, 2009|01:31 am]
Программирование с зависимыми типами

alexey_rom
[Tags|]

Изменения:
Классы типов (!)
Более производительные и новые библиотеки для арифметики
Много других изменений

Полное описание изменений
Качать
Link4 comments|Leave a comment

Знающие люди, подскажите! [Dec. 26th, 2008|01:22 pm]
Программирование с зависимыми типами

nivanych
Категорная модель higher order типов -- это топос.
Категорная модель зависимых типов -- это Local CCC.

Естественно, что все-все возможные системы
с зависимыми типами на практике не нужны.
Какие-то из них вполне впихиваются в топосы.

Так вот, меня взяло сомнение, а все ли "полезные"
системы типов могут упихаться в некоторый топос?...
Есть ли какая очень нужная и полезная система
с зависимыми типами, которая не описывается топосом
(топосом из топосов и функторов между ними)?...

ДополнениеCollapse )

P.S.
Надеюсь, это не оффтопик.
Есличо, подскажите, куда лучше запостить?...
Link2 comments|Leave a comment

Это не совсем про зависимые типы данных. [Dec. 24th, 2008|12:04 am]
Программирование с зависимыми типами

thesz
[Tags|, , ]

Type safe pattern matching combinators.

При чтении этой статьи у меня всё время было стойкое чувство, что я это видел в районе generic programming with dependent types.

К тому же там есть пример написания функции наподобие taut на этих комбинаторах.

Вот taut:
boolPower : {n : Nat} -> Set
boolPower Zero = Bool
boolPower (Succ n) = Bool -> boolPower n

taut : {n : Nat} -> boolPower n -> Bool
taut Zero v = v
taut (Succ n) f = taut n (f true) && taut n (f false)
Иными словами, функция, принимающая на вход функцию с произвольным числом аргументов.

И используемый в статье Хаскель очень простой, даже, по-моему, Haskell 98.
Link1 comment|Leave a comment

ATS -- новый фаворит на Great Language Shootout [Sep. 22nd, 2008|02:10 pm]
Программирование с зависимыми типами

geniepro
http://shootout.alioth.debian.org/u64q/benchmark.php?test=all&lang=all

ATS -- язык с зависимыми типами и си-подобным синтаксисом. По тестам на этом Шутауте программы на ATS в среднем на 20% шустрее, чем аналогичные на Си, причём разрыв доходит до 6.2 раза. Лишь а одном тесте программа на Си оказалась на 10% быстрее, чем на ATS.

Кто что думает об этом интересном проекте? Не это ли возможное будущее языков Си-семейства?

ЗЫ. Маленькое обсуждение на Реддите: http://www.reddit.com/r/programming/comments/72hmw/language_shootout_ats_is_the_new_top_gunslinger/

Комментарий автора языка:
...
Many people somehow think that ATS is fast because of its support for advanced types such as dependent types and linear types.

Actually, types are primarily for enhancing safety rather than speed. The efficiency of ATS is largely rooted in its data representation (flat instead of boxed) and its support for tail-call optimization, which is vital for a functional language.

To put it from a different angle, simply adding advanced types into an existing language can hardly improve its efficiency (but it can of course enhance its safety).

--Hongwei
Link7 comments|Leave a comment

Релизация функторной категории на Coq. [Sep. 5th, 2008|05:17 pm]
Программирование с зависимыми типами

thesz
[Tags|, ]

http://beroal.livejournal.com/9878.html
LinkLeave a comment

warez [Aug. 29th, 2008|09:59 am]
Программирование с зависимыми типами
hash_map
Наткнулся на варезную эл. книжку по Coq, авторства его создателей.

link
Страничка на Амазоне
Link2 comments|Leave a comment

navigation
[ viewing | 10 entries back ]
[ go | earlier/later ]