dependent type

• tek başına hayatta varolamayıp diğer insanların tepkileriyle var olabilen insan tipi. örn: popüler oliym da herkes benden bahsetsin, bölece varlıgımı kanıtlayım. örn2: tek başıma gezemiyorum, süper bi sevgilim olsun da öle varoliym. örn3: varolamıyom, irenç bişeyler yapıym da insanlar beni farketsin
• karşıtı için (bkz: otonom)
• bir de oyleleri vardir ki bunlarin, iliski insani tip olmaktan utanip, "ama yok benim x ile iliskimde biz ikimiz de codependentiz" deyiverirler sizin onlari yargilamaniza izin vermezcesine hizlica. ikimiz de birbirimize cok bagliyiz, ikimiz de birbirimizsiz zor yapariz demekmis iliski sozlugune codependant'lik. yeni trend bu, al birini vur otekine...
• elinizdeki verinin tipi uzerine veriye bagli constraintler ekleyebilmenizi saglayan type system modeli. bu sayede ornegin map fonksiyonunun aldigi liste ile ayni uzunlukta bir liste dondurmesini garanti altina alabilirsiniz. daha enterasan bir ornek ise i,j boyutlarinda bir matris ile j,k boyutlarinda bir matrisin carpiminin her zaman i,k boyutlarinda olacagini veri tipi seviyesinde garanti altina alabilirsiniz.
  
  (bkz: epigram)
  (bkz: dependent ml)
• (girizgah: basligin ilk entryleri konuyla cok alakasiz kalmis, aksam aksam semantik eksi sozluk mevzuunu hatirlayip uzuldum yine. gelelim asil konumuza.)
  (kodlarda bosluk yerine _ kullandim, buyuk harf de yok, kusura bakmayin.)
  
  fonksiyonel programlamada fonksiyonlarin birinci sinif vatandas olmasi gibi, tiplerin de birinci sinif vatandas oldugu sistem. (tek alametifarikasi bu degil ama giris icin iyi bir tanim). bu su anlama geliyor: fonksiyonlariniz sonuc olarak bir tip dondurebilir ve arguman olarak da bir tip alabilir. basit bir ornek verelim (agda sentaksiyla olacak) :
  
  dogal sayilar uzerinde bir esitlik tanimlayalim. oncelikle dogal sayilarin tanimi uzerinde bir uzlasalim:
  
  data nat : set where
  __z : nat
  __s : nat -> nat
  
  z sifiri, s ise arguman olarak aldigi sayiyi bir artiran bir fonksiyonu temsil ediyor. (bildigimiz peano sayilari)
  
  dilimizde curry-howard izomorfizmi'nden hatirladigimiz uzere, sadece tek bir deger alabilen bir unit tipi, ve hicbir deger alamayan void tipi oldugunu varsayalim.
  
  simdi esitligi tanimlayalim:
  
  equals : nat -> nat -> set
  equals z z = unit
  equals z (s m) = void
  equals (s n) z = void
  equals (s n) (s m) = equals n m
  
  artik isterseniz dogal sayilarla ilgili cesitli ozellikleri kanitlayacak fonksiyonlar yazabilirsiniz, ornegin dogal sayilarin gecisken oldugunu kanitlayan bir fonksiyonun tipi soyledir:
  
  transitive : (x : nat) -> (y : nat) -> (z -> nat) -> equals x y -> equals y z -> equals x z
  
  dependent typelar bunu yapmaniza izin verir. yapabileceginiz bir tik daha karmasik seyler: her islem sonunda sonuc olarak tum sartlara uymasi kod icinde kanitlanmis olan bir red-black tree implementasyonu. baska ornek: istenilen bir sekilde siralanmasi garantilenmis olan siralama algoritmasi implementasyonu. keyifli konular vesselam.
  
  edit ek: dependent type'larin tek getirdigi ozellik bu degil tabi. bu basitlestirilmis bir anlatimi.