типы-значения
May. 20th, 2013 03:12 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonНедавно я писал про простой шаг, добавляющий в систему типов обычного ФЯП зависимые типы: достаточно добавить один1 тип Type, элементами которого служат типы. Что занятно, из этого шага автоматически тут же следует первоклассность типов: они сразу же становятся обычными значениями, и их можно помещать в туплы, списки и т.д. и применять к ним обычные операции. Успешно компилирующийся в Идрисе пример:
По этой причине в Идрисе нет ключевого слова newtype. Чтобы определить синоним типа, достаточно описать его как значение (или как функцию, частный случай значения):
swap : (a,b) -> (b,a)
swap (a,b) = (b,a)
v : fst $ swap ("hi there", head [Int, String])
v = 42
По этой причине в Идрисе нет ключевого слова newtype. Чтобы определить синоним типа, достаточно описать его как значение (или как функцию, частный случай значения):
Matrix : Type -> Type Matrix a = List (List a) m : Matrix Int m = [[1,2], [3,4]]
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2013-05-20 09:06 am (UTC)Это прикольно, да)
no subject
Date: 2013-05-20 09:23 am (UTC)no subject
Date: 2013-05-20 09:54 am (UTC)42 : Int : Type0 : Type1 : Type2 : ...
и кумулятивность (Int : Type1, Int : Type2, ...).
Компилятор сам выводит и проверяет индексы в иерархии, а для программиста все эти вселенные называются Type.
no subject
Date: 2013-05-20 09:56 am (UTC)no subject
Date: 2013-05-20 10:32 am (UTC)no subject
Date: 2013-05-20 10:36 am (UTC)А во-вторых, для Prop оно меньше нужно. Впрочем, порасспрашиваю.
no subject
Date: 2013-05-24 04:13 pm (UTC)no subject
Date: 2013-05-24 05:18 pm (UTC)Например, в пределе, вопрос сведётся к нужности статической типизации ;-)
Где это используют — да полно. В агдочковой библиотеке, в основном, делают для любого Level'а, ну или для уровня l строят конструкцию Set (Succ l).
То есть, там вполне нормально обходят вопрос с уровнями.
Ну сейчас найду, где бы было Set1, например.
Вообще, обычно, это всякое около-мета.
Вот, например, из старого —
http://www.iis.sinica.edu.tw/~scm/2008/typed-lambda-calculus-interprete/
no subject
Date: 2013-05-24 08:32 pm (UTC)что вы, что вы :) я ж не отрицатель, я ж о "что мы теряем, если не можем"
я так чувствую, где-то нужно покурить про universes.
no subject
Date: 2013-05-25 05:27 am (UTC)http://code.haskell.org/~dolio/agda-share/hoas/PHOAS.agda
простая и полезная вещь, обратить внимание на
Term : Set1
Term = ∀{V} → term V
Хотя я щас понял, что такие вещи выводятся относительно просто и можно просто оперировать Set'ами.
То есть, для указания Set1 просто указываешь Set, а оно там разберётся, кто какого типа.
Когда этого может не хватить, чотта и затрудняюсь сказать. Ну и чем это хуже или лучше. По мне, так лучше явно SetN указывать, порядку больше ;-)
no subject
Date: 2013-05-20 09:57 am (UTC)Меня смутило "достаточно добавить один тип Type".
no subject
Date: 2013-05-20 10:47 am (UTC)Но предикативное непротиворечивым сделать проще.
no subject
Date: 2013-05-20 09:30 am (UTC)http://en.wikipedia.org/wiki/Cayenne_(programming_language)
no subject
Date: 2013-05-20 09:57 am (UTC)no subject
Date: 2013-05-20 10:04 am (UTC)Но мне показалось, что вполне так следует концепции в посте.
Из-за этого, можно и любой bottom заставить вычисляться в compile-time.
no subject
Date: 2013-05-20 10:00 am (UTC)no subject
Date: 2013-05-20 10:03 am (UTC)Самая главная няшка, это простота построения.
А неразрешимость относительно контролируема человеком. Точно так же, как и завершимость в runtime. В конце концов, макросы же как-то терпят? ;-)
no subject
Date: 2013-05-20 10:30 am (UTC)no subject
Date: 2013-05-20 10:35 am (UTC)no subject
Date: 2013-05-20 10:50 am (UTC)Вопрос в том, как доказывать свойства других полезных функций.
no subject
Date: 2013-05-26 10:35 am (UTC)а он уже доказал свою
бессмертностьнезавершимость?no subject
Date: 2013-05-26 10:43 am (UTC)no subject
Date: 2013-05-20 10:52 am (UTC)Построить башню из 3-4 доказательств завершимости предыдущей ступени и посчитать, что это достаточно надёжно!
;-)
no subject
Date: 2013-05-20 12:00 pm (UTC)Хоть type checking и не разрешим, он всё еще полуразрешим. Если вас очень волнует корректность можно всегда запустить type checker, который, если у вас всё хорошо, завершится с успехом, а если всё плохо, то либо сообщит об ошибке, либо зависнет.
И пусть зависающий компилятор вас не смущает, т.к. случайно написать зависающую программу у вас вряд ли получится. Даже при большом желании это не так просто, если не знать как. К тому же, и без Type:Type легко написать код, который повесит компилятор, хоть и не навечно, но фактически вы не дождетесь его завершения.
no subject
Date: 2013-05-21 04:47 am (UTC)Тов. Gregory Chaitin доказал, что вероятность зависания экспоненциально убывает с длиной программы ;-)
no subject
Date: 2013-05-20 10:11 am (UTC)no subject
Date: 2013-05-20 10:16 am (UTC)no subject
Date: 2013-05-20 10:21 am (UTC)no subject
Date: 2013-05-20 10:49 am (UTC)