Muhtemel durum geçişleri nasıl yazılır?

Question

Ben Haskell türleri üzerinden eylemlerin doğru sıralamasını zorlar İdris kodu, bu parça çoğaltmak çalışıyorum:

do Ring 
    Open 
    Close 

: (>>=) operatörün aşırı yüklemeye

data DoorState = DoorClosed | DoorOpen 
data DoorCmd : Type -> 
       DoorState -> 
DoorState -> 
       Type where 
     Open : DoorCmd () DoorClosed DoorOpen 
     Close : DoorCmd () DoorOpen DoorClosed 
     RingBell : DoorCmd() DoorClosed DoorClosed 
     Pure : ty -> DoorCmd ty state state 
     (>>=) : DoorCmd a state1 state2 -> 
       (a -> DoorCmd b state2 state3) -> 
       DoorCmd b state1 state3 

Teşekkür, tek gibi monadic kod yazabilirsiniz

ama derleyici gibi yanlış geçişleri reddeder: Ben bu modeli takip çalıştık

do Ring 
    Open 
    Ring 
    Open 

Aşağıdaki Haskell fragmanı: uygun işlemleri sıralamak için iki farklı örneğini gerektiren Applicative ve Monad örnekleri doğru olarak tanımlanamaz:

data DoorState = Closed | Opened 

data DoorCommand (begin :: DoorState) (end :: DoorState) a where 
    Open :: DoorCommand 'Closed 'Opened() 
    Close :: DoorCommand 'Opened 'Closed() 
    Ring :: DoorCommand 'Closed 'Closed() 

    Pure :: x -> DoorCommand b e x 
    Bind :: DoorCommand b e x -> (x -> DoorCommand e f y) -> DoorCommand b f y 

instance Functor (DoorCommand b e) where 
    f `fmap` c = Bind c (\ x -> Pure (f x)) 

-- instance Applicative (DoorCommand b e) where 
-- pure = Pure 
-- f <*> x = Bind f (\ f' -> Bind x (\ x' -> Pure (f' x'))) 

-- instance Monad (DoorCommand b e) where 
-- return = Pure 
-- (>>=) = Bind 

Fakat elbette bu başarısız

. Oluşturucu Bind doğru sıralama zorlamak için kullanılabilir ancak "güzel" do-notasyonu kullanmayı başaramıyorum.

Do-notasyonu kullanmak için bu kodu nasıl yazabilirim, ör. Command s geçersiz dizilerini önlemek için?

Answer 1

Neye bakıyorsunuz, atkey'in parameterised monad, şimdi daha yaygın olarak dizinli monad olarak bilinir.

class IFunctor f where 
    imap :: (a -> b) -> f i j a -> f i j b 
class IFunctor m => IMonad m where 
    ireturn :: a -> m i i a 
    (>>>=) :: m i j a -> (a -> m j k b) -> m i k b 

IMonad tek hücreli benzeri şeylerin sınıfı m :: k -> k -> * -> * tür k ait türleri yönlendirilmiş grafik üzerinden yolları tarif olup. >>>=, i - j için tür düzey durumunu j - k olarak alan bir hesaplama içine sokan bir hesaplama bağlar ve i - k için daha büyük bir hesaplama döndürür. ireturn, tür düzeyinde durumu değiştirmeyen tek bir değerde saf bir değer elde etmenizi sağlar.

ben istemiyorum büyük nedeni türü için IMonad örneği yazma anlamaya zorunda kalmak, istek-yanıt eylem bu tür yapısını yakalamak için endeksli ücretsiz monad kullanmak için gidiyorum kendim:

data IFree f i j a where 
    IReturn :: a -> IFree f i i a 
    IFree :: f i j (IFree f j k a) -> IFree f i k a 

instance IFunctor f => IFunctor (IFree f) where 
    imap f (IReturn x) = IReturn (f x) 
    imap f (IFree ff) = IFree $ imap (imap f) ff 
instance IFunctor f => IMonad (IFree f) where 
    ireturn = IReturn 
    IReturn x >>>= f = f x 
    IFree ff >>>= f = IFree $ imap (>>>= f) ff 

Biz şu funktor gelen ücretsiz olarak Door monad inşa edebilirsiniz:

data DoorState = Opened | Closed 
data DoorF i j next where 
    Open :: next -> DoorF Closed Opened next 
    Close :: next -> DoorF Opened Closed next 
    Ring :: next -> DoorF Closed Closed next 

instance IFunctor DoorF where 
    imap f (Open x) = Open (f x) 
    imap f (Close x) = Close (f x) 
    imap f (Ring x) = Ring (f x) 

type Door = IFree DoorF 

open :: Door Closed Opened() 
open = IFree (Open (IReturn())) 
close :: Door Opened Closed() 
close = IFree (Close (IReturn())) 
ring :: Door Closed Closed() 
ring = IFree (Ring (IReturn())) 

Sen open bir cur neden olan bir kapı, can Açıkça kapanan kapı açık olmak üzere, close bir açık kapı veya ring kapalı bir kapın zili, muhtemelen evin sakinleri sizi görmek istemediğinden dolayı.

Son olarak, RebindableSyntax dil uzantısı, standart Monad sınıfını kendi özel IMonad ile değiştirebileceğimiz anlamına gelir.

(>>=) = (>>>=) 
m >> n = m >>>= const n 
return = ireturn 
fail = undefined 

door :: Door Open Open() 
door = do 
    close 
    ring 
    open 

---

Ancak gerçekten monadın bağlayıcı yapısını kullanmıyor görüyoruz. Yapı taşlarınızın hiçbiri Open, Close veya Ring hiçbiri bir değer döndürmez. Yani ne gerçekten ihtiyacınız şu basit tip hizalanmış liste olduğunu düşünüyorum türü:

data Path g i j where 
    Nil :: Path g i i 
    Cons :: g i j -> Path g j k -> Path g i k 

Operasyonel olarak Path :: (k -> k -> *) -> k -> k -> * bağlantılı bir listesi gibi, ama bir kez daha açıklayan bazı ekstra tip düzeyinde bir yapıya sahiptir düğümleri k olan yönlendirilmiş bir grafikte yol. Listenin öğeleri g kenarlarıdır. Nil her zaman kendisine bir düğüm i bir yolunu bulabileceğini söylüyor ve Cons bin millik bir yolculuk tek bir adımla başlar hatırlatmaktadır: Eğer k için j den j için i bir kenar ve bir yol varsa, şunları yapabilirsiniz i'dan k'a yol yapmak için bunları birleştirin. Bu, türünde bir hizalanmış liste olarak adlandırılır, çünkü bir öğenin bitiş tipi bir sonraki başlangıç ​​türüyle eşleşmelidir. g ikili mantıksal ilişki ise o zaman Path g onun dönüşlü geçişli kapatma yapıları Curry-Howard Caddesi'nin diğer tarafında

. Veya, kategorik olarak,, g grafiğinin serbest kategorisi numaralı morfizm türüdür. Serbest kategorideki morfizmi oluşturmak, tipte hizalanmış listeleri ekleyerek sadece (çevrilir).

instance Category (Path g) where 
    id = Nil 
    xs . Nil = xs 
    xs . Cons y ys = Cons y (xs . ys) 

Sonra Path açısından Door yazabilirsiniz: (Sana liste değişmezleri aşırı izin vermezRebindableSyntax düşünmek gerçi)

data DoorAction i j where 
    Open :: DoorAction Closed Opened 
    Close :: DoorAction Opened Closed 
    Ring :: DoorAction Closed Closed 

type Door = Path DoorAction 

open :: Door Closed Opened 
open = Cons Open Nil 
close :: Door Opened Closed 
close = Cons Close Nil 
ring :: Door Closed Closed 
ring = Cons Ring Nil 

door :: Door Open Open 
door = open . ring . close 

Sen do gösterimini alamadım, ama bina hesaplamaları (.) ile, saf fonksiyonların sıralanması gibi görünüyor, ki zaten yaptığınız şey için oldukça iyi bir benzetme olduğunu düşünüyorum. Benim için endeksli monad kullanmak için ekstra bir beyin gücü (nadir ve değerli bir doğal kaynak) gerektirir. Daha basit bir yapı yapacağı zaman monadların karmaşıklığından kaçınmak daha iyidir.