Genelleştirilmiş cebirsel veri türü - Generalized algebraic data type

Olarak işlevsel programlama , bir genel cebirsel veri türü ( GADT da birinci sınıf fantom türü , korunan özyinelemeli veri türü veya eşitlik nitelikli tipi ) bir genellemedir parametrik cebirsel veri türleri .

genel bakış

Bir GADT'de, ürün oluşturucuları ( Haskell'de veri oluşturucuları olarak adlandırılır ), dönüş değerlerinin tür somutlaştırması olarak ADT'nin açık bir örneğini sağlayabilir. Bu, işlevlerin daha gelişmiş bir tür davranışıyla tanımlanmasına olanak tanır. Haskell 2010'un bir veri oluşturucusu için, dönüş değeri, yapıcının uygulamasında ADT parametrelerinin somutlaştırılmasıyla ima edilen tür örneklemesine sahiptir. 

-- A parametric ADT that is not a GADT
data List a = Nil | Cons a (List a)

integers = Cons 12 (Cons 107 Nil)       -- the type of integers is List Int
strings = Cons "boat" (Cons "dock" Nil) -- the type of strings is List String

-- A GADT
data Expr a where
    EBool  :: Bool     -> Expr Bool
    EInt   :: Int      -> Expr Int
    EEqual :: Expr Int -> Expr Int  -> Expr Bool

eval :: Expr a -> a

eval e = case e of
    EBool a    -> a
    EInt a     -> a
    EEqual a b -> (eval a) == (eval b)

expr1 = EEqual (EInt 2) (EInt 3)        -- the type of expr1 is Expr Bool
ret = eval expr1                        -- ret is False

Şu anda GHC derleyicisinde, diğerlerinin yanı sıra Pugs ve Darcs tarafından kullanılan standart olmayan bir uzantı olarak uygulanmaktadırlar . OCaml , 4.00 sürümünden beri GADT'yi yerel olarak destekler.

GHC uygulaması, varoluşsal olarak nicelleştirilmiş tür parametreleri ve yerel kısıtlamalar için destek sağlar.

Tarih

Genelleştirilmiş cebirsel veri türleri olan erken bir modeli tarafından tarif edilmiştir Augustsson ve Petersson (1994) ve göre desen eşleştirme olarak ALF .

Genelleştirilmiş cebirsel veri türleri ile, bağımsız bir şekilde tanıtıldı Cheney ve Hinze (2003) tarafından önceden Xi, Chen & Chen (2003) uzantıları olarak ML 'in ve Haskell sitesindeki cebirsel veri türleri . Her ikisi de özünde birbirine eşdeğerdir. Bunlar benzer veri tiplerinin endüktif ailesine (ya da indüktif veri türleri bulunan) Coq 'in Analiz Endüktif İnşa ve diğer bağımlı olarak yazılmış diller bağımlı türleri modulo ve ikinci ek olduğunu hariç, pozitif sınırlama GADTs zorlanmaz .

Sulzmann, Wazny ve Stuckey (2006) tanıtıldı cebirsel veri türleri uzatılmış birlikte GADTs kombine varoluş veri tiplerinin ve tip sınıfı ile ortaya kısıtlamalar Perry (1991) , Laufer ve Odersky (1994) ve Laufer (1996) .

Tür çıkarsama herhangi programcı verilen yokluğunda tip ek açıklamalar olduğunu undecidable ve GADTs üzerinde tanımlı fonksiyonlar kabul etmezler başlıca türleri genel olarak. Tip rekonstrüksiyonu birkaç tasarım değiş tokuşu gerektirir ve aktif bir araştırma alanıdır ( Peyton Jones, Washburn & Weirich 2004 ; Peyton Jones ve diğerleri 2006 ; Pottier & Régis-Gianas 2006 ; Sulzmann, Schrijvers & Stuckey 2006 ; Simonet & Pottier 2007 ; Schrijvers ve diğerleri 2009 ; Lin & Sheard 2010a ; Lin & Sheard 2010b ; Vytiniotis, Peyton Jones & Schrijvers 2010 ; Vytiniotis ve diğerleri 2011 ).

2021 baharında Scala 3.0 piyasaya sürüldü. Scala'nın bu büyük güncellemesi, Martin Odersky'ye göre diğer programlama dillerinde durum böyle olmayan, ADT'lerle aynı sözdizimine sahip GADT'leri yazma olanağı sunar .

Uygulamalar

GADTs uygulamaları içermektedir jenerik programlama programlama dilleri (modelleme, yüksek dereceden soyut sözdizimi koruyarak) değişmezleri içinde veri yapıları , içinde kısıtlamaları ifade eden gömülü alana özgü dilleri ve nesneleri modelleme.

Daha yüksek dereceli soyut sözdizimi

Daha fazla bilgi: Yüksek dereceli soyut sözdizimi

GADTs önemli bir uygulaması gömmektir yüksek mertebeden soyut sözdizimi bir de tip güvenli moda. İşte basit bir şekilde yazılan lambda hesabının rastgele bir temel tipler , demetler ve bir sabit nokta birleştirici koleksiyonuyla bir gömülmesi : 

data Lam :: * -> * where
  Lift :: a                     -> Lam a        -- ^ lifted value
  Pair :: Lam a -> Lam b        -> Lam (a, b)   -- ^ product
  Lam  :: (Lam a -> Lam b)      -> Lam (a -> b) -- ^ lambda abstraction
  App  :: Lam (a -> b) -> Lam a -> Lam b        -- ^ function application
  Fix  :: Lam (a -> a)          -> Lam a        -- ^ fixed point

Ve bir tür güvenli değerlendirme işlevi: 

eval :: Lam t -> t
eval (Lift v)   = v
eval (Pair l r) = (eval l, eval r)
eval (Lam f)    = \x -> eval (f (Lift x))
eval (App f x)  = (eval f) (eval x)
eval (Fix f)    = (eval f) (eval (Fix f))

Faktöriyel fonksiyon şimdi şu şekilde yazılabilir: 

fact = Fix (Lam (\f -> Lam (\y -> Lift (if eval y == 0 then 1 else eval y * (eval f) (eval y - 1)))))
eval(fact)(10)

Normal cebirsel veri türlerini kullanırken sorunlarla karşılaşırdık. type parametresinin düşürülmesi, yükseltilmiş baz tiplerinin varoluşsal olarak nicelenmesini sağlayarak değerlendiricinin yazılmasını imkansız hale getirirdi. Bir tür parametresi ile yine de tek bir temel türle sınırlandırılırdık. Ayrıca, App (Lam (\x -> Lam (\y -> App x y))) (Lift True)GADT kullanılarak yanlış yazılırken, oluşturulabilecek gibi kötü biçimli ifadeler . İyi biçimlendirilmiş bir analog App (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True)). Bunun nedeni, x is Lam (a -> b)türünün Lamveri oluşturucu türünden çıkarsanmasıdır .

Ayrıca bakınız

Notlar

daha fazla okuma

Uygulamalar
anlambilim
Tip rekonstrüksiyonu
Diğer

Dış bağlantılar