В. Н. Брагилевский (мехмат ЮФУ) Программирование с зависимыми типами на языке Idris 15/16. Список литературы. Curry–Howard correspondence. url: https


Чтобы посмотреть этот PDF файл с форматированием и разметкой, скачайте его и откройте на своем компьютере.
Ïðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìè
íàÿçûêåIdris
Ëåêöèÿ1.ÂåðèôèêàöèÿÏÎ,ñîîòâåòñòâèåÊàððèÕîâàðäà
èçàâèñèìûåòèïû
Â.Í.Áðàãèëåâñêèé
11ôåâðàëÿ2017ã.
ComputerScienceêëóá(Ñàíêò-Ïåòåðáóðã)
Èíñòèòóòìàòåìàòèêè,ìåõàíèêèèêîìïüþòåðíûõíàóê
èìåíèÈ.È.Âîðîâè÷à,Þæíûéôåäåðàëüíûéóíèâåðñèòåò(Ðîñòîâ-íà-Äîíó)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
1/16
Êîíòàêòû
ÂèòàëèéÁðàãèëåâñêèé
[email protected]
_bravit
bravit
bravit111
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
2/16
Ñòðóêòóðàêóðñà
ˆ
10ëåêöèé(5+5)
ˆ
GitHub-àêêàóíò
ˆ
2íàáîðàóïðàæíåíèéïóáëèêóþòñÿ13è20ôåâðàëÿ
ˆ
ýêçàìåíàöèîííûéïðîåêòïóáëèêóåòñÿ20ôåâðàëÿ
ˆ
ïðîâåðêàèîöåíèâàíèåïîÿâíîìóçàïðîñó(ïî÷òà:
íàïèøèòåâòåìåïèñüìàidris-spb,ñâîèôàìèëèþèèìÿ)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
3/16
Òèïûâÿçûêàõ
ïðîãðàììèðîâàíèÿ[Pierce,2002]
ÔîðìàëüíûåìåòîäûâðàçðàáîòêåÏÎ
Ñïåöèôèêàöèÿèïîâåäåíèåïðîãðàììû
ˆ
ñèñòåìûòèïîâ
ˆ
ôîðìàëüíûå
ïîäõîäûê
òåñòèðîâàíèþ
ˆ
ïðîâåðêàìîäåëåé
ˆ
SMT-ñîëâåðû
ˆ
àáñòðàêòíàÿ
èíòåðïðåòàöèÿ
ˆ
ìîíèòîðèíã
âðåìåíè
âûïîëíåíèÿ
ˆ
ëîãèêèÕîàðà
ˆ
ìîäàëüíûåëîãèêè
ˆ
ÿçûêè
àëãåáðàè÷åñêèõ
ñïåöèôèêàöèé
ˆ
äåíîòàöèîííûå
ñåìàíòèêè
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
4/16
ÔîðìàëüíûåìåòîäûâðàçðàáîòêåÏÎ
Ñïåöèôèêàöèÿèïîâåäåíèåïðîãðàììû
ˆ
ñèñòåìûòèïîâ
ˆ
ôîðìàëüíûå
ïîäõîäûê
òåñòèðîâàíèþ
ˆ
ïðîâåðêàìîäåëåé
ˆ
SMT-ñîëâåðû
ˆ
àáñòðàêòíàÿ
èíòåðïðåòàöèÿ
ˆ
ìîíèòîðèíã
âðåìåíè
âûïîëíåíèÿ
ˆ
ëîãèêèÕîàðà
ˆ
ìîäàëüíûåëîãèêè
ˆ
ÿçûêè
àëãåáðàè÷åñêèõ
ñïåöèôèêàöèé
ˆ
äåíîòàöèîííûå
ñåìàíòèêè
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
4/16
ÔîðìàëüíûåìåòîäûâðàçðàáîòêåÏÎ
Ñïåöèôèêàöèÿèïîâåäåíèåïðîãðàììû
ˆ
ñèñòåìûòèïîâ
ˆ
ôîðìàëüíûå
ïîäõîäûê
òåñòèðîâàíèþ
ˆ
ïðîâåðêàìîäåëåé
ˆ
SMT-ñîëâåðû
ˆ
àáñòðàêòíàÿ
èíòåðïðåòàöèÿ
ˆ
ìîíèòîðèíã
âðåìåíè
âûïîëíåíèÿ
ˆ
ëîãèêèÕîàðà
ˆ
ìîäàëüíûåëîãèêè
ˆ
ÿçûêè
àëãåáðàè÷åñêèõ
ñïåöèôèêàöèé
ˆ
äåíîòàöèîííûå
ñåìàíòèêè
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
4/16
ÔîðìàëüíûåìåòîäûâðàçðàáîòêåÏÎ
Ñïåöèôèêàöèÿèïîâåäåíèåïðîãðàììû
ˆ
ñèñòåìûòèïîâ
ˆ
ôîðìàëüíûå
ïîäõîäûê
òåñòèðîâàíèþ
ˆ
ïðîâåðêàìîäåëåé
ˆ
SMT-ñîëâåðû
ˆ
àáñòðàêòíàÿ
èíòåðïðåòàöèÿ
ˆ
ìîíèòîðèíã
âðåìåíè
âûïîëíåíèÿ
ˆ
ëîãèêèÕîàðà
ˆ
ìîäàëüíûåëîãèêè
ˆ
ÿçûêè
àëãåáðàè÷åñêèõ
ñïåöèôèêàöèé
ˆ
äåíîòàöèîííûå
ñåìàíòèêè
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
4/16
ÔîðìàëüíûåìåòîäûâðàçðàáîòêåÏÎ
Ñïåöèôèêàöèÿèïîâåäåíèåïðîãðàììû
ˆ
ñèñòåìûòèïîâ
ˆ
ôîðìàëüíûå
ïîäõîäûê
òåñòèðîâàíèþ
ˆ
ïðîâåðêàìîäåëåé
ˆ
SMT-ñîëâåðû
ˆ
àáñòðàêòíàÿ
èíòåðïðåòàöèÿ
ˆ
ìîíèòîðèíã
âðåìåíè
âûïîëíåíèÿ
ˆ
ëîãèêèÕîàðà
ˆ
ìîäàëüíûåëîãèêè
ˆ
ÿçûêè
àëãåáðàè÷åñêèõ
ñïåöèôèêàöèé
ˆ
äåíîòàöèîííûå
ñåìàíòèêè
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
4/16
Ñèñòåìûòèïîâ
Îïðåäåëåíèå[Pierce,2002]
Ñèñòåìàòèïîâýòîãèáêîóïðàâëÿåìûé
ñèíòàêñè÷åñêèéìåòîääîêàçàòåëüñòâàîòñóòñòâèÿâ
ïðîãðàììåîïðåäåëåííûõâèäîâïîâåäåíèÿïðè
ïîìîùèêëàññèôèêàöèèâûðàæåíèéÿçûêàïî
ðàçíîâèäíîñòÿìâû÷èñëÿåìûõèìèçíà÷åíèé.
ˆ
Ñòàòè÷åñêàÿòèïèçàöèÿ
ˆ
ïðîâåðêàòèïîâ(typechecking)
ˆ
âûâîäòèïîâ(typeinference)
ˆ
êîíñåðâàòèâíîñòü
ˆ
Äèíàìè÷åñêàÿïðîâåðêàòèïîâ
ˆ
îøèáêèòèïîââðåìåíèâûïîëíåíèÿ
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
5/16
Ñèñòåìûòèïîâ
Îïðåäåëåíèå[Pierce,2002]
Ñèñòåìàòèïîâýòîãèáêîóïðàâëÿåìûé
ñèíòàêñè÷åñêèéìåòîääîêàçàòåëüñòâàîòñóòñòâèÿâ
ïðîãðàììåîïðåäåëåííûõâèäîâïîâåäåíèÿïðè
ïîìîùèêëàññèôèêàöèèâûðàæåíèéÿçûêàïî
ðàçíîâèäíîñòÿìâû÷èñëÿåìûõèìèçíà÷åíèé.
ˆ
Ñòàòè÷åñêàÿòèïèçàöèÿ
ˆ
ïðîâåðêàòèïîâ(typechecking)
ˆ
âûâîäòèïîâ(typeinference)
ˆ
êîíñåðâàòèâíîñòü
ˆ
Äèíàìè÷åñêàÿïðîâåðêàòèïîâ
ˆ
îøèáêèòèïîââðåìåíèâûïîëíåíèÿ
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
5/16
Ñèñòåìûòèïîâ
Îïðåäåëåíèå[Pierce,2002]
Ñèñòåìàòèïîâýòîãèáêîóïðàâëÿåìûé
ñèíòàêñè÷åñêèéìåòîääîêàçàòåëüñòâàîòñóòñòâèÿâ
ïðîãðàììåîïðåäåëåííûõâèäîâïîâåäåíèÿïðè
ïîìîùèêëàññèôèêàöèèâûðàæåíèéÿçûêàïî
ðàçíîâèäíîñòÿìâû÷èñëÿåìûõèìèçíà÷åíèé.
ˆ
Ñòàòè÷åñêàÿòèïèçàöèÿ
ˆ
ïðîâåðêàòèïîâ(typechecking)
ˆ
âûâîäòèïîâ(typeinference)
ˆ
êîíñåðâàòèâíîñòü
ˆ
Äèíàìè÷åñêàÿïðîâåðêàòèïîâ
ˆ
îøèáêèòèïîââðåìåíèâûïîëíåíèÿ
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
5/16
Ïðåäíàçíà÷åíèåòèïîâ
ˆ
Âûÿâëåíèåîøèáîê
ˆ
Àáñòðàêöèÿ
ˆ
Äîêóìåíòàöèÿ
ˆ
Áåçîïàñíîñòü
ˆ
Ýôôåêòèâíîñòü
ˆ
Èíòåðàêòèâíàÿðàçðàáîòêà
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
6/16
Ïðåäíàçíà÷åíèåòèïîâ
ˆ
Âûÿâëåíèåîøèáîê
ˆ
Àáñòðàêöèÿ
ˆ
Äîêóìåíòàöèÿ
ˆ
Áåçîïàñíîñòü
ˆ
Ýôôåêòèâíîñòü
ˆ
Èíòåðàêòèâíàÿðàçðàáîòêà
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
6/16
Çàâèñèìûåòèïû
Çàâèñèìûåòèïû
äëÿïðîãðàììèñòîâ
Êëàññè÷åñêèéïðèìåð:âåêòîðûôèêñèðîâàííîãîðàçìåðà
Òèïâåêòîðà
Vect
:
Nat
�-
Type
�-
Type
Ïðèìåðâåêòîðà
v
:
Vect
3
Integer
v
=
[
10
,
5
,
1
]
Ôóíêöèèíàäâåêòîðàìè
cons
:
a
�-
Vect
n
a
�-
Vect
(
n
+
1
)
a
head
:
Vect
(
n
+
1
)
a
�-
a
vadd
:
Vect
n
a
�-
Vect
m
a
�-
Vect
(
n
+
m
)
a
Çàâèñèìûéòèï=òèï,çàâèñÿùèéîòçíà÷åíèÿ
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
7/16
Êëàññè÷åñêèéïðèìåð:âåêòîðûôèêñèðîâàííîãîðàçìåðà
Òèïâåêòîðà
Vect
:
Nat
�-
Type
�-
Type
Ïðèìåðâåêòîðà
v
:
Vect
3
Integer
v
=
[
10
,
5
,
1
]
Ôóíêöèèíàäâåêòîðàìè
cons
:
a
�-
Vect
n
a
�-
Vect
(
n
+
1
)
a
head
:
Vect
(
n
+
1
)
a
�-
a
vadd
:
Vect
n
a
�-
Vect
m
a
�-
Vect
(
n
+
m
)
a
Çàâèñèìûéòèï=òèï,çàâèñÿùèéîòçíà÷åíèÿ
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
7/16
Êëàññè÷åñêèéïðèìåð:âåêòîðûôèêñèðîâàííîãîðàçìåðà
Òèïâåêòîðà
Vect
:
Nat
�-
Type
�-
Type
Ïðèìåðâåêòîðà
v
:
Vect
3
Integer
v
=
[
10
,
5
,
1
]
Ôóíêöèèíàäâåêòîðàìè
cons
:
a
�-
Vect
n
a
�-
Vect
(
n
+
1
)
a
head
:
Vect
(
n
+
1
)
a
�-
a
vadd
:
Vect
n
a
�-
Vect
m
a
�-
Vect
(
n
+
m
)
a
Çàâèñèìûéòèï=òèï,çàâèñÿùèéîòçíà÷åíèÿ
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
7/16
Êëàññè÷åñêèéïðèìåð:âåêòîðûôèêñèðîâàííîãîðàçìåðà
Òèïâåêòîðà
Vect
:
Nat
�-
Type
�-
Type
Ïðèìåðâåêòîðà
v
:
Vect
3
Integer
v
=
[
10
,
5
,
1
]
Ôóíêöèèíàäâåêòîðàìè
cons
:
a
�-
Vect
n
a
�-
Vect
(
n
+
1
)
a
head
:
Vect
(
n
+
1
)
a
�-
a
vadd
:
Vect
n
a
�-
Vect
m
a
�-
Vect
(
n
+
m
)
a
Çàâèñèìûéòèï=òèï,çàâèñÿùèéîòçíà÷åíèÿ
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
7/16
Çàâèñèìûåòèïû
äëÿòåîðåòèêîâ
ÑîîòâåòñòâèåÊàððèÕîâàðäà
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
True
ëþáîéíàñåë¼ííûéòèï
False
?
(òèïáåççíà÷åíèé)
äîêàçàòåëüñòâî
òåðìòðåáóåìîãîòèïà,
a
:
A
A
^
B
(êîíúþíêöèÿ)
A

B
(ïðîèçâåäåíèå)
AB
A
^
B
a
:
Ab
:
B
(
a
;
b
):
A

B
A
_
B
(äèçúþíêöèÿ)
A
+
B
(ñóììà)
A
A
_
B
,
B
A
_
B
a
:
A
a
left
:
A
+
B
,
b
:
B
b
right
:
A
+
B
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
8/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
True
ëþáîéíàñåë¼ííûéòèï
False
?
(òèïáåççíà÷åíèé)
äîêàçàòåëüñòâî
òåðìòðåáóåìîãîòèïà,
a
:
A
A
^
B
(êîíúþíêöèÿ)
A

B
(ïðîèçâåäåíèå)
AB
A
^
B
a
:
Ab
:
B
(
a
;
b
):
A

B
A
_
B
(äèçúþíêöèÿ)
A
+
B
(ñóììà)
A
A
_
B
,
B
A
_
B
a
:
A
a
left
:
A
+
B
,
b
:
B
b
right
:
A
+
B
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
8/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
True
ëþáîéíàñåë¼ííûéòèï
False
?
(òèïáåççíà÷åíèé)
äîêàçàòåëüñòâî
òåðìòðåáóåìîãîòèïà,
a
:
A
A
^
B
(êîíúþíêöèÿ)
A

B
(ïðîèçâåäåíèå)
AB
A
^
B
a
:
Ab
:
B
(
a
;
b
):
A

B
A
_
B
(äèçúþíêöèÿ)
A
+
B
(ñóììà)
A
A
_
B
,
B
A
_
B
a
:
A
a
left
:
A
+
B
,
b
:
B
b
right
:
A
+
B
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
8/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
True
ëþáîéíàñåë¼ííûéòèï
False
?
(òèïáåççíà÷åíèé)
äîêàçàòåëüñòâî
òåðìòðåáóåìîãîòèïà,
a
:
A
A
^
B
(êîíúþíêöèÿ)
A

B
(ïðîèçâåäåíèå)
AB
A
^
B
a
:
Ab
:
B
(
a
;
b
):
A

B
A
_
B
(äèçúþíêöèÿ)
A
+
B
(ñóììà)
A
A
_
B
,
B
A
_
B
a
:
A
a
left
:
A
+
B
,
b
:
B
b
right
:
A
+
B
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
8/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà(2)
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
A
!
B
(èìïëèêàöèÿ)
A
!
B
(òèïôóíêöèè)
AA
!
B
B
(modusponens)
a
:
Af
:
A
!
B
f
(
a
):
B
(âûçîâ)
:
A
A
!?
Ïðåäèêàò
P
(
x
)
,
x
2
X
8
x
2
XP
(
x
)
9
x
2
XP
(
x
)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
9/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà(2)
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
A
!
B
(èìïëèêàöèÿ)
A
!
B
(òèïôóíêöèè)
AA
!
B
B
(modusponens)
a
:
Af
:
A
!
B
f
(
a
):
B
(âûçîâ)
:
A
A
!?
Ïðåäèêàò
P
(
x
)
,
x
2
X
8
x
2
XP
(
x
)
9
x
2
XP
(
x
)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
9/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà(2)
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
A
!
B
(èìïëèêàöèÿ)
A
!
B
(òèïôóíêöèè)
AA
!
B
B
(modusponens)
a
:
Af
:
A
!
B
f
(
a
):
B
(âûçîâ)
:
A
A
!?
Ïðåäèêàò
P
(
x
)
,
x
2
X
8
x
2
XP
(
x
)
9
x
2
XP
(
x
)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
9/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà(2)
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
A
!
B
(èìïëèêàöèÿ)
A
!
B
(òèïôóíêöèè)
AA
!
B
B
(modusponens)
a
:
Af
:
A
!
B
f
(
a
):
B
(âûçîâ)
:
A
A
!?
Ïðåäèêàò
P
(
x
)
,
x
2
X
8
x
2
XP
(
x
)
9
x
2
XP
(
x
)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
9/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà(2)
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
A
!
B
(èìïëèêàöèÿ)
A
!
B
(òèïôóíêöèè)
AA
!
B
B
(modusponens)
a
:
Af
:
A
!
B
f
(
a
):
B
(âûçîâ)
:
A
A
!?
Ïðåäèêàò
P
(
x
)
,
x
2
X
çàâèñèìûéòèï,
T
:
X
!
Type
8
x
2
XP
(
x
)
9
x
2
XP
(
x
)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
9/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà(2)
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
A
!
B
(èìïëèêàöèÿ)
A
!
B
(òèïôóíêöèè)
AA
!
B
B
(modusponens)
a
:
Af
:
A
!
B
f
(
a
):
B
(âûçîâ)
:
A
A
!?
Ïðåäèêàò
P
(
x
)
,
x
2
X
çàâèñèìûéòèï,
T
:
X
!
Type
8
x
2
XP
(
x
)

x
:
X
T
(
x
)
,çàâèñèìàÿôóíêöèÿ
9
x
2
XP
(
x
)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
9/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà(2)
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
A
!
B
(èìïëèêàöèÿ)
A
!
B
(òèïôóíêöèè)
AA
!
B
B
(modusponens)
a
:
Af
:
A
!
B
f
(
a
):
B
(âûçîâ)
:
A
A
!?
Ïðåäèêàò
P
(
x
)
,
x
2
X
çàâèñèìûéòèï,
T
:
X
!
Type
8
x
2
XP
(
x
)

x
:
X
T
(
x
)
,çàâèñèìàÿôóíêöèÿ
9
x
2
XP
(
x
)

x
:
X
T
(
x
)
,çàâèñèìàÿïàðà
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
9/16
ÑîîòâåòñòâèåÊàððèÕîâàðäà(2)
Âûñêàçûâàíèå
A
Òèï
A
èñòèííîëèáîëîæíî
íàñåë¼íëèáîíåò
A
!
B
(èìïëèêàöèÿ)
A
!
B
(òèïôóíêöèè)
AA
!
B
B
(modusponens)
a
:
Af
:
A
!
B
f
(
a
):
B
(âûçîâ)
:
A
A
!?
Ïðåäèêàò
P
(
x
)
,
x
2
X
çàâèñèìûéòèï,
T
:
X
!
Type
8
x
2
XP
(
x
)

x
:
X
T
(
x
)
,çàâèñèìàÿôóíêöèÿ
9
x
2
XP
(
x
)

x
:
X
T
(
x
)
,çàâèñèìàÿïàðà
x
2
Xt
2
T
(
x
)

x
;
t

:
x
:
X
T
(
x
)
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
9/16
PapersweloveâÑàíêò-Ïåòåðáóðãå
ˆ
https://vk.com/paperswelovespb
ˆ
PhilipWadler,Propositionsastypes
ˆ
÷åòâåðã,16ôåâðàëÿ,20:00
ˆ
êîâîðêèíã¾ÂÊîíòàêòå¿íàÊàçàíñêîéóëèöå,7
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
10/16
Idris:îáùàÿõàðàêòåðèñòèêà
ßçûêïðîãðàììèðîâàíèÿIdris
Idrisýòîêîìïèëèðóåìûé,÷èñòîôóíêöèîíàëüíûé
ÿçûêîáùåãîíàçíà÷åíèÿñçàâèñèìûìèòèïàìèè
ñòðîãèìâû÷èñëåíèåì.
EdwinBrady,UniversityofStAndrews
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
11/16
ßçûêïðîãðàììèðîâàíèÿIdris
Idrisýòîêîìïèëèðóåìûé,÷èñòîôóíêöèîíàëüíûé
ÿçûêîáùåãîíàçíà÷åíèÿñçàâèñèìûìèòèïàìèè
ñòðîãèìâû÷èñëåíèåì.
EdwinBrady,UniversityofStAndrews
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
11/16
ÎñíîâíûåýëåìåíòûÿçûêàIdris
ˆ
Ïîëíîöåííûåçàâèñèìûåòèïûñçàâèñèìûì
ñîïîñòàâëåíèåìñîáðàçöîì
ˆ
Ïðîñòîéèíòåðôåéñêâíåøíèìôóíêöèÿì(íàC)
ˆ
Ïîääåðæêàðåäàêòèðîâàíèÿêîäàâêîìïèëÿòîðåíàîñíîâå
òèïîâ
ˆ
Áëîêè
where
,ïðàâèëà
with
,
case
-âûðàæåíèÿ,
ñîïîñòàâëåíèåñîáðàçöîìâ
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
12/16
ÎñíîâíûåýëåìåíòûÿçûêàIdris(2)
ˆ
Óïðàâëÿåìîåòèïàìèðàçðåøåíèåïåðåãðóçêè
ˆ
do
-íîòàöèÿèñêîáêè
[|.|]
ˆ
Ñèíòàêñèññîçíà÷èìûìèîòñòóïàìè
ˆ
Ðàñøèðÿåìûéñèíòàêñèñ
ˆ
Êóìóëÿòèâíûéóíèâåðñóì-òèï
ˆ
Ïðîâåðêàòîòàëüíîñòè
ˆ
ÈíòåðàêòèâíîåîêðóæåíèåâñòèëåHugs
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
13/16
Ïðèìåðïðîãðàììû
module
Main
average
:(
str
:
String
)�-
Double
average
str
=
num_words
=
word_count
str
total_length
=
sum
(
word_lengths
(
words
str
))
in
cast
total_length
/
cast
num_words
where
word_count
:
String
�-
Nat
word_count
str
=
length
(
words
str
)
word_lengths
:
List
String
�-
List
Nat
word_lengths
strs
=
map
length
strs
showAverage
:
String
�-
String
showAverage
str
=
"Ñðåäíÿÿäëèíà:"
++
show
(
average
str
)
++
"\n"
main
:
IO
()
main
=
repl
"Ââåäèòåñòðîêó:"
showAverage
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
14/16
ÃîòîâëèIdrisêproduction?
ˆ
Ñìîòðÿ÷òîñ÷èòàòüproduction!
ˆ
Ïðîáëåìà1:ñòàáèëüíîñòüÿçûêà(òåêóùàÿâåðñèÿ0.99)
ˆ
Ïðîáëåìà2:âîçìîæíà(î÷åíü)äîëãàÿêîìïèëÿöèÿ
ˆ
Ïðîáëåìà3:îøèáêèâêîìïèëÿòîðå(ïðîâåðêà
òîòàëüíîñòè,äîêàçàòåëüñòâî
?
)
ˆ
Ïðîáëåìà4:(ïî÷òè)íåòáèáëèîòåê
ˆ
ÇàòîåñòüêíèæêàType-drivenDevelopmentinIdris(Edwin
Brady,Manning)ìàðò2017
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
15/16
ÃîòîâëèIdrisêproduction?
ˆ
Ñìîòðÿ÷òîñ÷èòàòüproduction!
ˆ
Ïðîáëåìà1:ñòàáèëüíîñòüÿçûêà(òåêóùàÿâåðñèÿ0.99)
ˆ
Ïðîáëåìà2:âîçìîæíà(î÷åíü)äîëãàÿêîìïèëÿöèÿ
ˆ
Ïðîáëåìà3:îøèáêèâêîìïèëÿòîðå(ïðîâåðêà
òîòàëüíîñòè,äîêàçàòåëüñòâî
?
)
ˆ
Ïðîáëåìà4:(ïî÷òè)íåòáèáëèîòåê
ˆ
ÇàòîåñòüêíèæêàType-drivenDevelopmentinIdris(Edwin
Brady,Manning)ìàðò2017
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
15/16
ÃîòîâëèIdrisêproduction?
ˆ
Ñìîòðÿ÷òîñ÷èòàòüproduction!
ˆ
Ïðîáëåìà1:ñòàáèëüíîñòüÿçûêà(òåêóùàÿâåðñèÿ0.99)
ˆ
Ïðîáëåìà2:âîçìîæíà(î÷åíü)äîëãàÿêîìïèëÿöèÿ
ˆ
Ïðîáëåìà3:îøèáêèâêîìïèëÿòîðå(ïðîâåðêà
òîòàëüíîñòè,äîêàçàòåëüñòâî
?
)
ˆ
Ïðîáëåìà4:(ïî÷òè)íåòáèáëèîòåê
ˆ
ÇàòîåñòüêíèæêàType-drivenDevelopmentinIdris(Edwin
Brady,Manning)ìàðò2017
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
15/16
ÃîòîâëèIdrisêproduction?
ˆ
Ñìîòðÿ÷òîñ÷èòàòüproduction!
ˆ
Ïðîáëåìà1:ñòàáèëüíîñòüÿçûêà(òåêóùàÿâåðñèÿ0.99)
ˆ
Ïðîáëåìà2:âîçìîæíà(î÷åíü)äîëãàÿêîìïèëÿöèÿ
ˆ
Ïðîáëåìà3:îøèáêèâêîìïèëÿòîðå(ïðîâåðêà
òîòàëüíîñòè,äîêàçàòåëüñòâî
?
)
ˆ
Ïðîáëåìà4:(ïî÷òè)íåòáèáëèîòåê
ˆ
ÇàòîåñòüêíèæêàType-drivenDevelopmentinIdris(Edwin
Brady,Manning)ìàðò2017
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
15/16
ÃîòîâëèIdrisêproduction?
ˆ
Ñìîòðÿ÷òîñ÷èòàòüproduction!
ˆ
Ïðîáëåìà1:ñòàáèëüíîñòüÿçûêà(òåêóùàÿâåðñèÿ0.99)
ˆ
Ïðîáëåìà2:âîçìîæíà(î÷åíü)äîëãàÿêîìïèëÿöèÿ
ˆ
Ïðîáëåìà3:îøèáêèâêîìïèëÿòîðå(ïðîâåðêà
òîòàëüíîñòè,äîêàçàòåëüñòâî
?
)
ˆ
Ïðîáëåìà4:(ïî÷òè)íåòáèáëèîòåê
ˆ
ÇàòîåñòüêíèæêàType-drivenDevelopmentinIdris(Edwin
Brady,Manning)ìàðò2017
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
15/16
ÃîòîâëèIdrisêproduction?
ˆ
Ñìîòðÿ÷òîñ÷èòàòüproduction!
ˆ
Ïðîáëåìà1:ñòàáèëüíîñòüÿçûêà(òåêóùàÿâåðñèÿ0.99)
ˆ
Ïðîáëåìà2:âîçìîæíà(î÷åíü)äîëãàÿêîìïèëÿöèÿ
ˆ
Ïðîáëåìà3:îøèáêèâêîìïèëÿòîðå(ïðîâåðêà
òîòàëüíîñòè,äîêàçàòåëüñòâî
?
)
ˆ
Ïðîáëåìà4:(ïî÷òè)íåòáèáëèîòåê
ˆ
ÇàòîåñòüêíèæêàType-drivenDevelopmentinIdris(Edwin
Brady,Manning)ìàðò2017
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
15/16
Ñïèñîêëèòåðàòóðû
CurryHowardcorrespondence
.
url
:
https:
//en.wikipedia.org/wiki/Curry-Howard_correspondence
.
Idris:ALanguagewithDependentTypes
.
url
:
http://www.idris-lang.org/
.
Pierce,BenjaminC.(2002).
TypesandProgrammingLanguages
.
Èìååòñÿðóññêèéïåðåâîä:Òèïûâÿçûêàõïðîãðàììèðîâàíèÿ,
Ìîñêâà,2012.
Â.Í.Áðàãèëåâñêèé(ìåõìàòÞÔÓ)
ÏðîãðàììèðîâàíèåñçàâèñèìûìèòèïàìèíàÿçûêåIdris
16/16

Приложенные файлы

  • pdf 7736642
    Размер файла: 637 kB Загрузок: 0

Добавить комментарий