Pengetahuan atau pelatihan apa yang diperlukan seseorang untuk menuliskan definisi foldlM seperti ini? [Tutup]

Baru-baru ini, saya mencoba menggunakan Haskell di beberapa sistem produksi kasus nyata saya. Sistem tipe Haskell benar-benar menawarkan saya bantuan besar. Sebagai contoh, ketika saya menyadari bahwa saya memerlukan beberapa fungsi tipe

f :: (Foldable t, Monad m) => ( a-> b -> m b) -> b -> t a -> m b

Sebenarnya ada fungsi seperti foldM, foldlMdan foldrM.

Namun, yang sangat mengejutkan saya adalah definisi dari fungsi-fungsi ini, seperti:

foldlM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
foldlM f z0 xs = foldr f' return xs z0
  where f' x k z = f z x >>= k

jadi fungsi f'harus bertipe:

f' :: a -> b -> b

seperti yang disyaratkan foldr, maka bharus dari jenis *-> m *, sehingga seluruh definisi foldlMbisa masuk akal.

Contoh lain termasuk definisi liftA2dan<*>

(<*>) :: f (a -> b) -> f a -> f b
(<*>) = liftA2 id

liftA2 :: (a -> b -> c) -> f a -> f b -> f c
liftA2 f x = (<*>) (fmap f x)

Saya mencoba beberapa solusi saya sendiri sebelum mengintip ke dalam kode sumber. Tetapi celahnya sangat besar sehingga saya tidak berpikir saya bisa menemukan solusi ini, tidak peduli berapa banyak baris kode yang akan saya tulis di masa depan.

Jadi pertanyaan saya adalah, pengetahuan seperti apa atau cabang matematika spesifik apa yang diperlukan seseorang untuk bernalar pada tingkat yang sangat abstrak.

Saya tahu Teori Kategori mungkin menawarkan bantuan dan saya telah mengikuti kuliah yang luar biasa ini sejak lama dan masih mengerjakannya.

Secara umum, dll logika, saya akan membayangkan. Tetapi Anda juga dapat mempelajarinya dengan melakukannya. :) Dengan waktu Anda memperhatikan beberapa pola, ambil beberapa trik.

Seperti ini foldrdengan argumen tambahan. Beberapa melihatnya sebagai fungsi lipat sehingga mereka dapat digabungkan melalui .dan id(yang kadang - kadang benar-benar <=<dan return),

foldr g z xs  =  foldr ($) z . map g $ xs
              =  foldr (.) id (map g xs) z
         ~/=  foldr (<=<) return (map g xs) z
{-
  (\f -> f . f) :: (a -> a) -> (a -> a)

  (\f -> f <=< f) :: Monad m => (a -> m a) -> (a -> m a)
                            (still just a type, not a kind)
-}

Beberapa merasa lebih mudah untuk memahaminya dalam istilah sintaksis yang lebih sederhana

foldr g z [a,b,c,...,n] s =
     g a (foldr g z [b,c,...,n]) s

jadi ketika gtidak ketat dalam argumen kedua, sbisa berfungsi sebagai keadaan yang diteruskan dari kiri, meskipun kita melipat di sebelah kanan, sebagai salah satu contoh.

Jadi cara terbaik untuk memahaminya adalah dengan melakukannya. Di bawah ini ada implementasi foldlMpenggunaanfoldl alih-alih foldr. Ini latihan yang bagus, coba dan dapatkan solusi yang saya sarankan. Contoh menjelaskan semua alasan yang saya lakukan untuk mencapainya, yang mungkin berbeda dari Anda, dan mungkin bias karena saya sudah tahu tentang menggunakan fungsi akumulator.

Langkah 1 : Mari kita coba menulis foldlMdalam bentukfoldl

-- this doesn't compile because f returning type is (m b) and not just (b) 
foldlM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
foldlM f z0 xs = foldl f z0 xs 

-- So let substitute f by some undefined f'
foldlM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
foldlM f z0 xs = foldl f' z0 xs
  where f' = undefined

-- cool, but f' should use f somehow in order to get the monadic behaviour
foldlM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
foldlM f z0 xs = foldl f' z0 xs
  where f' b a = f somethingIDontkNow 

Di sini Anda menyadari bahwa f'itu murni dan Anda harus mengekstraksi hasil fmengetik. Satu-satunya cara untuk 'mengekstraksi' nilai monadik adalah dengan>>= operator, tetapi operator seperti itu harus dibungkus tepat setelah digunakan.

Jadi sebagai kesimpulan: Setiap kali Anda berakhir dengan saya ingin sepenuhnya membuka monad ini , menyerah saja. Bukan jalan yang benar

Langkah 2 : Mari kita coba menulis foldlMdalam bentuk foldltetapi pertama menggunakan []sebagai lipat, karena mudah untuk mencocokkan pola (yaitu kita tidak benar-benar perlu menggunakan fold)

-- This is not very hard. It is pretty standard recursion schema. :)
foldlM' :: (Monad m) => (b -> a -> m b) -> b -> [a] -> m b
foldlM' f z0 []     = return z0
foldlM' f z0 (x:xs) = f z0 x >>= \c -> foldlM' f c xs

Oke, itu mudah. Mari kita bandingkan definisi dengan foldldefinisi biasa untuk daftar

foldlM' :: (Monad m) => (b -> a -> m b) -> b -> [a] -> m b
foldlM' f z0 []     = return z0
foldlM' f z0 (x:xs) = f z0 x >>= \c -> foldlM' f c xs

myfoldl :: (b -> a -> b) -> b -> [a] -> b
myfoldl f z0 []     = z0
myfoldl f z0 (x:xs) = foldl f (f z0 x) xs

Keren!! mereka hampir sama. Kasus sepele adalah tentang hal yang persis sama. Kasus rekursif adalah sedikit berbeda sedikit, Anda ingin menulis sesuatu yang lebih seperti: foldlM' f (f z0 x) xs. Tetapi tidak dikompilasi seperti pada langkah 1, jadi Anda mungkin berpikir OK, saya tidak ingin menerapkan f, hanya untuk memegang perhitungan seperti itu dan menyusunnya >>=. Saya ingin menulis sesuatu yang lebih suka foldlM' f (f z0 x >>=) xs jika itu masuk akal ...

Langkah 3 Sadarilah bahwa yang ingin Anda kumpulkan adalah komposisi fungsi dan bukan hasil. (di sini saya mungkin bias oleh fakta bahwa saya sudah mengetahuinya karena Anda telah mempostingnya ).

foldlM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
foldlM f z0 xs = foldl f' initFunc xs
  where initFunc = undefined :: b -> m b
        f'       = undefined :: (b -> m b) -> a -> (b -> m b) -- This type signature can be deduce because f' should be applied to initFunc and a's from t a. 

Dengan tipe initFuncdan menggunakan pengetahuan kita dari langkah 2 (definisi rekursif) kita dapat menyimpulkan itu initFunc = return. Definisi f'dapat diselesaikan mengetahui yang f'harus digunakan fdan >>=.

foldlM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
foldlM f z0 xs = foldl f' return xs z0
--                        ^^^^^^
--                        |- Initial value
  where f' b a = \bvalue -> b bvalue >>= \bresult -> f bresult a -- this is equivalent to (b >=> \result -> f result a) which captures the sequence behaviour of the implementation
--         ^      ^^^^^^                  ^^^^^^^
--         |      |                       |- This is the result of previous computation
--         |      |- f' should return a function b -> m b. Any time you have to return a function, start writing a lambda  
--         |- This b is the accumulated value and has type b -> m b
-- Following the types you can write this with enough practise

Seperti yang Anda lihat, tidak sangaaaat sulit untuk melakukannya. Itu perlu latihan, tapi saya bukan pengembang haskell profesional dan saya bisa melakukannya sendiri, ini soal latihan

Anda tidak perlu pengetahuan khusus dalam matematika untuk menulis fungsi seperti foldM. Saya menggunakan Haskell dalam produksi selama 4 tahun, dan saya juga berjuang untuk memahami definisi ini foldM. Tetapi itu sebagian besar karena itu ditulis dengan buruk. Tolong, jangan menganggapnya sebagai kesalahan pribadi jika Anda tidak dapat memahami beberapa kode yang tidak jelas. Ini adalah versi yang lebih mudah dibaca darifoldlM

foldlM
    :: forall t m a b .
       (Foldable t, Monad m)
    => (b -> a -> m b)  -- ^ Monadic action
    -> b                -- ^ Starting accumulator
    -> t a              -- ^ List of values
    -> m b              -- ^ Computation result inside a monad
foldlM f z xs = (foldr step pure xs) z
  where
    step :: a -> (b -> m b) -> b -> m b
    step cur next acc = do
        result <- f acc cur
        next result

Fungsi ini masih bukan yang termudah. Sebagian besar karena memiliki penggunaan non-khas di foldrmana akumulator menengah adalah suatu fungsi. Tetapi Anda dapat melihat beberapa orang yang membuat definisi seperti itu lebih mudah dibaca:

1. Komentar tentang argumen fungsi.
2. Nama argumen yang lebih baik (masih pendek dan idiomatis, tetapi setidaknya lebih mudah dibaca).
3. Jenis tanda tangan eksplisit dari fungsi di dalam where(sehingga Anda tahu bentuk argumen).

Setelah melihat fungsi seperti itu, Anda sekarang dapat melakukan teknik penalaran Equasional untuk memperluas definisi langkah demi langkah dan melihat cara kerjanya. Kemampuan untuk datang dengan fungsi seperti itu datang dengan pengalaman. Saya tidak memiliki keterampilan matematika yang kuat, dan fungsi ini bukan fungsi Haskell yang khas. Tetapi semakin banyak latihan yang Anda miliki, semakin baik :)