Copatterns
Motivation So, what are copatterns, and why do we want them? Essentially, copatterns allow us to make projections on the left-hand side of function definitions. Left-hand side projections make sense for definitions from which we primarily want to extract data, contrary to injecting data into data constructors. Examples include record types and coinductive types. Observation vs. Construction Copatt
copatterns概要 - ぼくのぬまち 出張版
ghc-7.8でビルドできるAgdaマダカナーとか思いつつ，Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら，実験的機能としてcopatternsってやつが入ると書かれている．余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつつ読むと，なにやらこんなカンジのようだ． タプルをレコードで定義すると，次のようになる． record _×_ (A B : Set) : Set where constructor _,_ field fst : A snd : B open _×_タプルのフィールドとしては1番目の要素であるfstと2番目の要素であるsndを持っていて，recordをopenすればこれらは普通に関数として使える． 通常，タプルを与えるような関数は最終的にタプルをコンストラクトすることになる． pair : {A B : Set} →
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Agda copatterns (Release notes for Agda 2 version 2.3.4)
