February 15, 2013 - Tagged as: ocaml, types, tr.
Bu yazı birkaç gün önce attığım bir mail aslında. Acele ile yazılmış bir yazı olmasına rağmen epey uzun oldu ve maili yazmaya başlamadan önce kafamda karmaşık bir şekilde duran bazı fikirleri toparlamamda yardımcı oldu. Pek kimsenin işine yarayacağını tahmin etmesem de, yine de buraya koyuyorum. Küçük bazı düzenlemeler yaptım. Eklemeler ise yazının en altına yazıldı. Kodlar OCaml dilinde yazıldı.
Üzerinde çalıştığım dilin tip sistemi hakkında1:
type ty =
| ...
| TRow of tyrow
| ...
type fieldty =
| Pre ty
| Btm (* Abs ismi lambda abstractionlarda kullanildi *)
type tyrow =
| EmptyRow
| Row (id * ty * ..1..)
| ..2..1 ve 2 boşluklarını doldurmamız gerekiyor. Sorunlar şunlar:
1 kısmına yazdığımız tip, sadece yine kendi tipiyle(yani TRow ile) unify etmek zorunda(ilk bakışta tyrow yazmak mantıklı gibi geliyor ama bu yüzden değil).
2 kısmına yazdığımız constructor polymorphic row’u temsil edecek. Burada ben ilk başta aslında row değişkenlerini tamamen yok sayıp, recordlar extensible mı değil mi diye bir boolean flag tutayım demiştim. Fakat sorun, recordlar rowları paylaşabiliyorlar, örneğin şöyle bir fonksiyonda \r -> r.x = 10 tip {r/x} -> {x:int|r/x} oluyor, başka bir yerde bu r kullanılabilir(parametre olarak verilen record başka yerlerde kullanıldığında fonksiyonun dönüş değeri olan recordın row değişkeni ile aynı row değişkenine sahip birden fazla record oluyor). Dolayısıyla bir değişken olmak zorunda.
Fakat bu typevar tipinde olamaz, çünkü typevar bir ty ile unify edilebiliyor. Rowlarda ise tyrow ile unify etmek istiyoruz. Ayrı bir tip gerekiyor yani.
Temel olarak row variable ile normal variable tamamen aynı olmalı, tek farkla, row değişkenler sadece row değişkenlerle/değerler ile unify edecek, variablelar da aynı şekilde.2
Type schemeler row değişkenler de tutabilir. let ile bir fonksiyon tanımladım, fonksiyon tipindeki free type variableları generalize ederek(terimler teminoloji ile uyumlu olsun diye ingilizce kullanıldı) bu fonksiyon polymorphic hale getiriliyor ve tipi TypeScheme olarak tutuluyor, quantified değişkenler belirtiliyor.3
Daha sonra bu fonksiyon kullanıldığında instantiate ediliyor. Burada instantiate edilen quantified değişkenler yerine ancak kendi kindlarında tiplerin konulması bir şekilde sağlanmalı.
Yani şunu demeye çalışıyorum, elimde bir row variable varsa, bu ancak bir row tipi ile yer değiştirebilir(yerine ancak row tipi yazılabilir). Bunu implementasyon sırasında tip sistemi ile garanti etmek gerçekten zor. İnsanlar bu yüzden kind sistemi kullanıyorlar sanırım.
Kind kullanırsam şöyle oluyor, her tipe bir kind veriyorum. Özet geçmek gerekirse, mesela TVar bir type değişkeni tutuyordu, şimdi bir de kind tutacak. Kindlar ise dilimde kaç tip -birbirlerinden farklı- type varsa, o kadar olacak. Örneğin Star int, bool gibi tipler için kullanılırken, Row row tipleri için kullanılır. Bu sayede bir değişkenim Row kindında ise, quantified edilse de instantiate edilse de bu bilgi taşınır ve en son yerine yazılacağında kind kontrol edilir. Tüm yerine yazmalar kind-preserving olmalıdır.4
Bu sayede farklı kindlarda type variablelar için aynı fonksiyonları kullanabilirim, sürekli kind bilgisini de taşırım. En son substitution veya unification yaparken, kindların korunup korunmadığını kontrol ederim ve normal type değişkeni yerine row type yazılmamasını sağlarım veya unification sırasında hata alırım.
–
Kindlarla beraber tipleri şu şekilde tanımlayabiliyoruz(yaklaşık olarak, henüz programı yazmadım)
type kind =
| KStar (* kind of term types *)
| KRow (* kind of row types *)
| KArr of (kind * kind) (* kind of type constructors *)
type ty =
| TCon of tycon (* constant *)
| TVar of tyvar (* type variable *)
| TApp of (ty * ty)
(* type application, to be well-typed
kind of first ty should be KArr (k2, k)
and second ty should be k2 *)
and tyvar = (tyvarlink ref * kind)
and tyvarlink =
| NoLink of id (* just a type variable *)
| LinkTo of ty (* equated to a ty *)
and tycon = (id * kind) (* kind should be always KStar *)
let t_int = TCon ("int", KStar)
let t_bool = TCon ("bool", KStar)
let t_unit = TCon ("unit", KStar)
let t_list = TCon ("[]", KArr (KStar, KStar))
let t_ref = TCon ("ref", KArr (KStar, KStar))
let t_arr = TCon ("->", KArr (KStar, KArr (KStar, KStar)))
let t_empty_row = TCon ("<|>", KRow)
let t_row_ext = TCon ("<+>", KArr (KStar, KArr (KRow, KRow)))
let t_rec_const = TCon ("{_}", KArr (KRow, KStar))
(* type of {r1} *)
let rp1 = TApp (t_rec_const, TVar (ref (NoLink "r1"), KRow))
(* type of {r1} -> {_:int|r1} *)
let f = TApp (TApp (t_arr, rp1), TApp (TApp (t_row_ext, t_int), rp1))En sonraki iki tanım örnek olsun diyeydi.
Karmaşık olduğunun farkındayım ama 1) bu tip sistemi implementasyonları için standard yol gibi geldi bana(çok fazla makalede kind sistemlerinden bahsediliyor) 2) diğer türlü de daha az karmaşık değil gibi.5
Burda mesela TApp oluşturan bir yardımcı fonksiyon oluştururuz ve kindları kontrol eder, uyumlu mu diye, bir miktar daha kolaylaşır. Yardımcı fonksiyonlarla işi kolaylaştırabiliriz diye düşünüyorum yani.
Bu örnekde rp1 yerine mesela {a:bool} (yani TApp (TApp (t_rec_ext, bool_ty), t_empty_row)) yazarsak:
TApp (TApp (t_arr, rp1), TApp (TApp (t_row_ext, t_int), TApp (TApp (t_rec_ext, bool_ty), t_empty_row)))Bana gayet temiz bir şekilde {x:int, a:bool} elde ettik gibi geliyor ve tek yaptığımız yerine yazmak oldu. ( bu sunumda labelların atlandığının farkındayım, tam olarak labelları nasıl bu sisteme entegre ederim düşünmedim )
Diğer türlü yapılamaz mı, tabii ki yapılabilir ve ben zaten çok yaklaşmıştım. Fakat çirkin olmayan bir yolu yok. Kod içerisinde şöyle kısımlar olmak zorunda gibi: “implementasyonum doğru olduğuna göre bu type variable record ile unify edilmiş olacak, exhaustive olmayan pattern matching yap”. Mesela tüm row değişkenler bir record’a unify edilimş olacak, ben pattern matching ile fieldları alacağım kendi recordıma ekleyeceğim vs.6
Ama kindler ile yaptığımda bu gibi durumlar olmayacak, ben TApp’lar ile typelar oluşturacağım, kind preserving substitutionlar, generalizationlar, instantiationlar yapılacağından, her zaman row tiplerim well-formed olmuş olacak ben hiçbir kontrol yapmadan TApp’ler oluşturmaya başlayacağım.
Ben bugün akşam birkaç makale daha inceleyeceğim: Type Inference for Records in a Natural Extension of ML (Didier Rémy) ve A Polymorphic Type System for Extensible Records and Variants (Mark P. Jones, Benedict R. Gaster). Bir de Typing Haskell in Haskell (Mark P. Jones)’a baktım, Haskell’da burada konuştuğumuz anlamda recordlar yok, ama kind sisteminden bahsederken “row kindlar da kolayca eklenebilir” diyerek sanırım yukarıda yaptığım şeyi kastetmekte.
Bu nasıl olabiliyor anlayabilmiş değilim ama gerçekten internette hiç örnek implementasyon yok. Bu yüzden ben bir tane yazacağım blog yazısı olarak. Polymorphic recordlara sahip bir dil inceleyeyim dedim, bir tanesi Elm adlı bir dil, kaynağı Haskell ile yazılmış temel olarak “Scoped Labels” makalesini kullanmış, ama kod berbat bir durumda. Çok çok karmaşık, kod stili berbat(type annotationlarını atlamış, Haskell’da bunu hiçbir zaman yapmayız, derleyici uyarı verir, annotationlar OCaml’daki gibi kodun içine yazılmaz, ayrı bir satıra yazılır ve anlaşılabilmeye çok katkı sağlarlar) vs. Yine de okunacak olursa en mantıklısı bu.
İkincisi SML#. Bu da ne yazık ki SML üzerine implement edilmiş ve kaynak kodu devasa. Tüm SML kodunu incelemek gerekecek yani(aradım bulamadım alakalı kısımları).7
Özetle, row polymorphism’e sahip, multi-staged bir dil. Buradaki veri yapısı dilin tip sistemini ifade ediyor. Row tiplerine dikkat. Row polymorphism’de fieldlar üzerinde bazı kısıtlar tanımlamanın birkaç yolu var. Bir yol, benim burada yaptığım ve D. Rémy’nin “Type inference for records in a natural extension of ML” ve başka makalelerinde gösterdiği gibi, field tiplerinde bir çeşit “flag” tutmak. Makalelerde Abs/Pre diye geçer, benim kodumda Pre/Btm. Bu yolun bu işi yapmak en bariz yol olduğunu söyleyebiliriz belki. Fakat kesinlikle en kolay/güzel yötem değil. Alternatif olarak kısıtlar constraint seviyesinde, kind seviyesinde veya başka bazı seviyelerde tanımlanabiliyor.↩︎
Burada anlatmaya çalıştığım problem bana çok vakit kaybettirdi ve aslında pek çok kişiye tanıdık gelebilir. Kısaca yapmaya çalıştığım şey, bazı şeyleri statik olarak garanti etmek için tip sistemini kullanmaya çalışmak. Örneğin bir programlama dilinde syntax ağacını well-formed olmayan programları ifade edebilmesini engelleyecek şekilde oluşturmak gibi. Bu gibi durumlarda eğer yeterince güçlü tip sisteminiz yoksa(örnek: GADTler yardımcı olabiliyor) işiniz çok zorlaşabiliyor. Daha kolay bir yöntemi runtime’da bunu garantilemek. Hemen sonrasında anlattığım şey tam olarak bu aslında. Statik garantiler verebilmek süper birşey aslında. Hiçbir şart altında programınızın yanlış çalışmayacağını garanti altına alıyorsunuz. Ama bazı durumlarda bu mümkün ama çok zor olabiliyor. Diğer yandan, zor da olsa bir kere implement ettikten sonra kesin olarak doğru çalışacağından emin olabiliyorsunuz. Veya test etmesi çok kolay oluyor vs.↩︎
Anlattığım şey Damas-Hindley-Milner tip sisteminin temellerinden aslında.↩︎
Kindları kendi kendime keşfettiğim an. Aslında Haskell programcısı olduğumdan kind konspetine aşinaydım, ama bu şekilde kullanımı bir bakıma kendi kendime keşfettim diyebilirim. Kind adını da ben vermedim tabii, daha sonra hakkında okudukça farkettim.↩︎
“diğer türlü daha az karmaşık değil gibi” derken kastettiğim, Rémy usulü, field tiplerine bir flag koyarak Abs/Pre özelliğini belirtmekti.↩︎
Burda aslında biraz programımın implementasyonu ile alakalı detaylardan bahsediyorum. Belki bir ara biraz daha açarım.↩︎
Daha sonradan farkettim ki bir alternatif daha varmış: “Extensible records with scoped labels” makalesinde bahsedilenlerin implement edildiği Morrow programlama dili. En iyi implementasyon şimdilik bu. Tek problemi, kurulmak için UUAG attribute grammar systema ihtiyaç duyması. Bir de eğer sadece type inference yapmasın, bir de çalıştırsın derseniz, OCaml’a ihtiyaç duyuyor. Evet çok fantastik. Haskell ile statik analiz kısımları yapılıyor ve OCaml’a derleniyor. Tabii programın asıl olayı tip sistemi olduğundan, deneme için yazdığınız programları çalıştırmak istemeyebilirsiniz, o zaman OCaml’a gerek yok.↩︎