GADTs

Question

kullanarak "güvenli liste" için kuyruk fonksiyonu a GADT walkthrough üzerinden okuyordum ve alıştırmalardan birine takılı kaldım. Belirli bir veri yapısı şöyledir:

{-# LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-} 
data NotSafe 
data Safe 
data MarkedList :: * -> * -> * where 
    Nil :: MarkedList t NotSafe 
    Cons :: a -> MarkedList a b -> MarkedList a c 

egzersiz bir safeTail fonksiyonunu uygulamaktır.

safeTail (Cons 'c' (Cons 'a' (Cons 't' Nil))) == Cons 'a' (Cons 't' Nil) 
safeTail (Cons 'x' Nil)      == Nil 
safeTail Nil -- type error (not runtime!) 

^{(Aslında == tanımlamak yoktu, ama umarım ne demek istediğimi açık)}

bu

yapılabilir: Ben Prelude tail işlevine benzer hareket etmek istiyorum? Türün ne olabileceğinden emin değilim ... belki de safeTail :: MarkedList a Safe -> MarkedList a NotSafe?

Answer 1

tip yapısını biraz değiştirirseniz safeTail uygulamak mümkündür:

{-# LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-} 

data Safe a 
data NotSafe 

data MarkedList :: * -> * -> * where 
    Nil :: MarkedList t NotSafe 
    Cons :: a -> MarkedList a b -> MarkedList a (Safe b) 

safeHead :: MarkedList a (Safe b) -> a 
safeHead (Cons h _) = h 

safeTail :: MarkedList a (Safe b) -> MarkedList a b 
safeTail (Cons _ t) = t 

orijinal safeTail :: MarkedList a Safe -> MarkedList a b sorun b herhangi bir tür olabilir ki - ille aynı tip olduğu kuyruk liste ile işaretlenir. Bu, safeTail geri dönüş türünün uygun şekilde kısıtlanmasına izin veren tip seviyesindeki liste yapısını yansıtarak burada düzeltilmiştir.

Answer 2

Evet, bu yapılabilir. Hile varoluşsal olarak sayılan içerilen listeyi bilinen bir tür listeye dönüştürmektir: özellikle bir NotSafe bir!

unsafe :: MarkedList a b -> MarkedList a NotSafe 
unsafe Nil = Nil 
unsafe (Cons a b) = Cons a b 

Şimdi güvenle kuyruk alabilir:

safeTail :: MarkedList a Safe -> MarkedList a NotSafe 
safeTail (Cons a b) = unsafe b 

Ayrıca, bu desen maç tamamlandı. -fwarn-incomplete-patterns'dan bir uyarı almayacaksınız ve bir Nil yan tümcesi eklemeye çalışırsanız bir hata alırsınız. en bir Show örneği türetmek, StandaloneDeriving açın ve örnekleri test edelim: Beş dakika öncesine kadar bölümden bağlandı çözüm açıkça yanlış olduğunu

*Main> safeTail (Cons 'c' (Cons 'a' (Cons 't' Nil))) 
Cons 'a' (Cons 't' Nil) 
*Main> safeTail (Cons 'x' Nil) 
Nil 
*Main> safeTail Nil 

<interactive>:10:10: 
    Couldn't match type `NotSafe' with `Safe' 
    Expected type: MarkedList a0 Safe 
     Actual type: MarkedList a0 NotSafe 
    In the first argument of `safeTail', namely `Nil' 
    In the expression: safeTail Nil 
    In an equation for `it': it = safeTail Nil