deniok

Как лучше делать сопоставление с образцом в языке с зависимыми типами?

Coq's inductive types are implemented using separate "match" and "fix" constructions, which allow for deep matching, mutual matching, etc. Similarly, Agda allows function definition by pattern matching with a separate termination checker. However, this approach is only justified semantically by translating it into eliminators, and it is hard to make sense of for higher inductive types. On the other hand, deep matching is very useful for functional programmers.

One potential solution to this problem is the approach used in Epigram, where there is a "pattern matching" syntax that is extensible rather than baked into the system. Any term whose type has "the form of an induction principle" can be used to justify a pattern-matching syntax. Thus, although each inductive definition comes with its defining induction principle, the user can prove their own new induction principles (such as for deep matching, mutual recursion, etc.) and then use those elimination rules with the same sort of pattern-matching syntax.

This may be especially nice for higher inductive types, where preliminary experiments suggest that there can be meaningful notions of "deep recursion" and "mutual recursion" in particular cases, but it seems difficult to give one general formulation of such principles.

Crossposts: http://deni-ok.livejournal.com/47486.html

Ура!

thesz таки запустил Epigram и нас научил! Вот мой Hello World:

------------------------------------------------------------------------------
                                          (   n : Nat    !
data (---------!  where (------------! ;  !--------------!
     ! Nat : * )        ! zero : Nat )    ! succ n : Nat )
------------------------------------------------------------------------------
inspect succ (zero) => succ zero : Nat
------------------------------------------------------------------------------
     (   x, y : Nat   !                  
let  !----------------!                  
     ! plus x y : Nat )                  
                                         
     plus x y <= case x                  
     { plus zero y => y                  
       plus (succ x) y => succ (plus x y)
     }                                   
------------------------------------------------------------------------------
inspect plus (succ (succ zero)) (succ (succ zero)) => ? : Nat
------------------------------------------------------------------------------

Как, блин, редактировать исходники пока непонятно... Они в XEmacs'е, сволочи, интерактивные (что удобно), но после успешного заэскейпливания сараев переходят в readonly режим :(

Такую красоту (Epigram: Practical Programming with Dependent Types) нельзя не изучить!

Пойду, куплю картриджи для цветного принтера :-)

UPD: Why Dependent Types Matter - ещё ссылочка про него.

Википедия про Epigram

Сайт языка Epigram

S	M	T	W	T	F	S
		1	2	3	4	5
6	7	8	9	10	11	12
13	14	15	16	17	18	19
20	21	22	23	24	25	26
27	28

Entries tagged with epigram

Цитата для памяти

Epigram в действии!

Epigram

Profile

February 2022

Syndicate

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags