Dinamik olarak statik olarak yazılan diller hakkında çok fazla yayılma oldu. Ancak, benim gözümde, statik olarak yazılan diller, derleyicinin (veya yorumlayıcınızın) niyetleriniz hakkında biraz daha fazla bilgi sahibi olmasını sağlarken, yalnızca nelerin iletilebileceğinin yüzeyini çizebilir. Aslında, bazı diller ek açıklamalarda daha fazla bilgi sağlamak için ortogonal bir mekanizmaya sahiptir.Beyond tip teorisi
Agda ve Coq gibi çok yazılan dillerden biliyorsunuz; Ben bunlarla çok ilgilenmiyorum. Aksine, derleyiciye neyi niyet ettiğiyle ilgili açıklayabileceğin zenginliklerini genişleten hangi dillerin veya teorinin var olduğunu merak ediyorum. Örneğin, mutable vektörüne sahipseniz ve bunu bir birim vektörüne dönüştürdüğünüzde, derleyiciniz daha hesaplamalı olarak daha pahalı genel form yerine bir vektör vektörü projeksiyon biçimi seçemedi? Tür değişmedi - ve gerekli tüm türlerin oluşturulması için gerekli olan işler Haskell gibi inanılmaz derecede kolay bir yazımla bile bir dilde yayınlanacaktı - ve yine de derleyicinin büyük bir şey bilmek için yetkilendirilmiş olduğu anlaşılıyor. durum hakkında.
Bazı diller zaten standart tip teorisinin dışında veya daha gelişmiş dallarından birinde böyle şeyleri etkinleştirir mi?
Niçin Agda ve Coq'la ilgileniyorsanız, tam olarak ne sundukları (ne kadar az pratik bir eğilim olsa da, ancak Idris daha pratik bir direktöre gidiyor). ? Belli türdeki vektörler için zekice bir temsili örneğiniz, Haskell'in vektör kütüphanesi tarafından zaten sağlanmıştır. Ayrıca LiquidHaskell ve Dana Xu'nun GHC'deki sözleşmelerle ilgili daha önceki çalışmaları ile de ilgilenebilirsiniz. – copumpkin
@copumpkin - Belki ilgimi çekmeliyim, ancak gördüğüm tüm örnekler ne kadar yararlı olduklarını çok net bir şekilde görebiliyorlar ve bunları muğlak ve nesnel yönelimli bir bağlamda nasıl genişletebileceğimi göremiyorum. trickier alır ve yine de daha fazla yardıma ihtiyacınız var. –
@Rex Bağımlılardan daha anlamlı bir soyutlama mı arıyorsunuz? Eğer öyleyse, bir örnek sunabilir misin? Aksi takdirde, belki de bunu tatmin edici bir şekilde uygulayan bir dil arıyorsanız. –