Simpler, Easier! no'lu makalede, "Pi" nin varlığı olmadan bile bağımlı sistemlerin kodlanması mümkün olabilir - yani, bunun için "Lam" yapıcısını yeniden kullanabilirsiniz. Ancak "Pi" ve "Lam" bazı durumlarda farklı muamele görürse, bu nasıl doğru olabilir?Aslında "Pi" Yapı Taşları'ndan çıkarmak mümkün mü?
Ayrıca "Yıldız" kaldırılabilir mi? Sanırım tüm olayları "λ x. X" (id) ile değiştirebilirsiniz.
Bu sadece Haskell'de (a, b) gibi aşırı yükleme yapıyor: hem bir tür hem de bir değer olabilir. Aynı bağlayıcıyı Π ve λ için de kullanabilirsiniz ve typechecker, hangisini istediğinizi belirleyecektir. Başka karşı bir bağlayıcı typecheck, o zaman eski λ ve ikincisi Π - ve sen açık bir şekilde λ x . x ile * yerini alamaz bu yüzden - sonra eski bağlayıcı Π olabileceğinden ve ikincisi bir bağlayıcı olarak * (* olduğunu bana hiç mantıklı gelmiyor). ∀ = λ ve * = λ x . x ile daha büyük bir sorun var: False'u yayınlamak için yaygın bir yol olan transitlik * = ∀ x . x - bu tür bir ses sisteminde iskan edilmemelidir, bu nedenle hiç türünüz olmayacaktır.
Dominic Mulligan:
http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf
: burada
Ve küçük bir kaynakça benzer işe bakacak şekilde başka bir şeydir İronik olarak, bu makaleye göre Coquand, AutoMath'te De Bruijn tarafından oluşturulan bir sözleşmesini takiben, Constructions of Calculus'u tek, birleşik bir bağlayıcı ile sundu.
Thorsten Altenkirch:
bir fonksiyon ve tip onlar bazı yüzeysel sözdizimsel benzerlik olsa bile çok farklı kavramlardır. Özellikle yeni gelenler için bu tanımlama çok kafa karıştırıcı ve tamamen yanıltıcıdır. Birinin nasıl göründüğünden değil, nasıl göründüğüne göre teorik kavramlarını anlaması gerektiğini düşünüyorum.
Andreas Abel:
, "Tip türleri olmadan kontrol etme"
Not olduğunu Matthias Benkard da böyle bir sistem üzerinde çalıştı
Öğrencim İlk linkte açıklanan sistem Π-redüksiyona sahiptir (örn.Pi-tiplerini lambdas gibi uygulayabilirsiniz) - Sisteminiz de Π ve λ'u içsel olarak (sözdizimsel olarak değil) birleştirirseniz sisteminiz de olacaktır. Ve ikinci bağlantı açıklanan sistem tipleri birleştirir ve değer
dolaysız bir sonucu türleri ve yaşayanlar arasında herhangi bir fark olmaması: her bir değer kendisi ve parçaları her ihtiva eden bir tür; ve tersine, her tür, sakinlerinden oluşan kompozit bir değerdir.
böylece gerçekten (let ve belki fix hariç) sadece bir bağlayıcı yoktur.
Üzgünüz, ne zaman bir Pi olması gerektiğini ve ne zaman bir bağlam olması gerektiğinin farkında değilsiniz. Ayrımla ilgili biraz detaylandırır mısınız? – MaiaVictor
Basit bir örnek olarak, 'λ (a: *) -> λ (x: a) -> a' kendisine uygulanır. Ne olurdu? A: * 've her şey bir tür olduğundan, bu terim her şeyi kabul etmez mi? – MaiaVictor
@Viclib, Ben temel bir bağımlı tip teorisi için küçük bir typechecker var, ben 'Π' ve' λ' birleştirmeye çalışacağız. Eğer [a: *] -> [x: a] -> a 'varsa ve bunu kendinize uygularsanız, ilk ciltçi bir lambda gibi davranır ve sonuç [x: [a: *] -> [x: a] -> a] -> a'. – user3237465