Haskell Wiki varoluşsal türlerinin nasıl kullanılabileceğini açıklayan iyi bir iş yok, ama oldukça onları arkasındaki teori grok bilmiyorum.

Varoluşsal bir tür bu örneği ele alalım

data S = forall a. Show a => S a      -- (1)

bir tür tanımlamak için String dönüştürmek şeyler için sarıcı. Wiki ne biz bahsedergerçektentanımlamak ister gibi bir tip

data S = S (exists a. Show a => a)    -- (2)

yani gerçek bir "veri S herhangi bir tür Show örneği . bir alır yapıcı" tür - gevşek söylediğim gibi bu bence varoluşsal ^strong>varve o". sarar Aslında, muhtemelen aşağıdaki gibi bir GADT yazabilirsiniz

data S where                          -- (3)
    S :: Show a => a -> S

Bu derleme denemedim, ama çalışması gerekir gibi görünüyor. Bana, GADT yazmak istediğimiz kodu besbelli eşdeğer (2).

Ancak, (2) eşdeğerdir benim için değil neden tamamen açık (1). Neden dış veri yapıcı hareket exists içine forall tahrik mi ediyor?

Aklıma en yakın şey bir olumsuzluk ve konarak sırası değiştirilerek evrensel nicelik içine varoluşsal nicelik döndüğü mantık De Morgan's Laws ya da tam tersi

¬(∀x. px) ⇔ ∃x. ¬(px)

ama veri kurucular olumsuzluk operatör için tamamen farklı bir canavar gibi görünüyor.

Varoluşsal türleri olmayan exists yerine forall kullanarak tanımlama yeteneği yatan teori nedir?

Öncelikle, bir bak "Howard" bir bilgisayar programı türleri modelleme ve analiz yapma mantığı. formüller tekabül eden bu yazışma Köri Modelleme ve analiz yapma mantığı "" mantık orta veya çifte olumsuzluk hariç kaldırılması Kanunu olmadan okulda ama öğrendim: . normal gibi

• Bir aksiyom: P ⇔ P (ama P Harflerle P iyidir)

• Bir aksiyom: P ∨ P

Mantık yasaları

DeMorgan yasaları ile doğru yolda, ama önce onlara yenilerini elde etmek için kullanacağız. DeMorgan kanunla ilgili sürümü

• ∀x. P(x) = $ x. P(x)
• $ x. P(x) = ∀x. P(x)

Türetmek (∀x. biz P harflerle Q(x)) = (∀x. harflerle P Q(x)):

1. (∀x. Q(x)) P harflerle
2. (∀x. Q(x)) P ∨
3. P ∨ (∀x. Q(x))
4. P harflerle (∀x. S)

Ve (∀x. (X) Q ⇒ P) = ($x. Q(x)) P (bunun altında kullanılır) harflerle:

1. (∀x. Q(x) P harflerle)
2. (∀x. Q(x) P∨)
3. (∀x. Q(x)) ∨ P
4. ($x. Q(x)) ∨ P
5. ($x. Q(x)) harflerle P

Bu yasalar, modelleme ve analiz yapma mantığı da basılı tutun unutmayın. Biz türetilmiş iki yasanın gazetede aşağıda belirtilmiştir.

Basit Türleri

En basit türleri ile çalışmak kolaydır. Örneğin:

data T = Con Int | Nil

Kurucular ve set aşağıdaki tür imzaları:

Con :: Int -> T
Nil :: T

unCon :: T -> Int
unCon (Con x) = x

Yazın Kurucular

Şimdi mücadele türü kurucular. Aşağıdaki veri tanımı:

data T a = Con a | Nil

Bu iki kurucular oluşturur

Con :: a -> T a
Nil :: T a

Haskell tabii, yazın değişkenleri örtülü olarak bu gerçekten çok evrensel inceledi

Con :: ∀a. a -> T a
Nil :: ∀a. T a

Ve erişimci aynı şekilde kolaydır:

unCon :: ∀a. T a -> a
unCon (Con x) = x

Türleri sayılabilir

Varoluşsal nicelik belirteci, ∃, orijinal türü (birinci tip kurucu olmadan) ekleyelim. Mantık benzemiyor hangi tip tanımı, katmak yerine, mantık benziyorum hangi erişimci tanımları / kurucu duyurmadan. Veri tanımı sonraki maç için düzelteceğiz.

* *31, yerine şimdi ∃x. t kullanacağız. Burada, t tür ifade gibi.

Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)

Mantık kurallarına göre (ikinci kural yukarıda), Con türüne yazabilirsiniz:

Con :: ∀x. t -> T

Dış varoluşsal nicelik belirteci (prenex form) taşındığımızda, evrensel bir nicelik belirteci dönüştü.

Aşağıdaki teorik olarak eşdeğerdir:

data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil

Dışında orada Haskell exists hiçbir sözdizimi.

Olmayan modelleme ve analiz yapma mantığı, caiz unCon türünden aşağıdaki elde edilir:

unCon :: ∃ T -> t -- invalid!

Bu geçersiz bir neden böyle bir dönüşüm modelleme ve analiz yapma mantığı izin verilmez çünkü. İmkansız exists bir anahtar kelime olmadan unCon türü yazmak ve imkansız prenex tipi şeklinde imza koydu. Zor bir türü denetleyicisi Haskell keyfi varoluşsal nicelik desteklemiyor neden olan bu koşullar, durdurmak için emin olun.

Kaynaklar

"Birinci sınıf Türü ile Polimorfizmi Kesmesi", Mark P. Jones, 24 ACM Yargılamanın SİGPLAN-SİGACT programlama dillerinin Prensipleri (web) Sempozyumu