2013-09-21 30 views
6

Tôi đang cố gắng hòa giải định nghĩa Phân loại của Monad với các biểu diễn/định nghĩa chung khác mà tôi đã thấy trong một số hướng dẫn/sách khác.Monads từ mọi góc độ - Toán học, sơ đồ và chương trình

Dưới đây, tôi (có lẽ mạnh mẽ) cố gắng để mang lại hai định nghĩa chặt chẽ, xin vui lòng chỉ ra những sai lầm và cung cấp sửa chữa, nơi nào cần

Vì vậy Bắt đầu với định nghĩa của Monads

Monads chỉ là monoids trong thể loại endofunctors.

và với một sự hiểu biết ít endofunctors, tôi giả sử một đơn nguyên có thể được viết như

((a->b)->Ma->Mb)->((b->c)->Mb->Mc) 

Các 'Type' của LHS (phía bên tay trái) là Mb, và loại RHS là Mc, vì vậy tôi cho rằng tôi có thể viết nó như sau

Mb-> (b->c)-> Mc, **which is how we define bind** 

Và đây là làm thế nào tôi thấy Monads trong danh mục của endofuctors (mà mình đang có trong Category C, với 'types' là objects)

Monad Visually.

Có bất kỳ điều này có ý nghĩa không?

Trả lời

9

Ừm, tôi nghĩ bạn có một chút nghỉ ngơi. Một đơn nguyên là một endofunctor, trong Hask (loại Haskell) là một loại có kiểu F :: * -> * với một số hàm biết cách chèn morphisms (functions) vào danh mục con của Hask với hàm số F s làm morphisms và F s đối tượng, fmap. Những gì bạn có ở đó dường như là một sự biến đổi tự nhiên trong Hask.

Ví dụ: Maybe, Either a, (,) a, vv ..

Bây giờ một đơn nguyên cũng phải có 2 biến đổi tự nhiên (Functor F, Functor g => F a -> G a trong hask).

n : Identity -> M 
u : M^2 -> M 

Hoặc trong mã Haskell

n :: Identity a -> M a -- Identity a == a 
u :: M (M a) -> M a 

tương ứng với returnjoin tương ứng.

Bây giờ, chúng tôi phải truy cập >>=. Những gì bạn có như là ràng buộc thực sự chỉ là fmap, những gì chúng tôi thực sự muốn là m a -> (a -> m b) -> m b. Điều này có thể dễ dàng được xác định là

m >>= f = join $ f `fmap` m 

Tada! Chúng tôi có các monads. Bây giờ cho monoid endofunctors này.

Một monoid trên endofunctors sẽ có một functors là đối tượng và biến đổi tự nhiên như hình thái. Điều thú vị là sản phẩm của hai endofunctors là thành phần của họ.Dưới đây là các mã Haskell cho monoid mới của chúng tôi

type (f <+> g) a = f (g a) 
class Functor m => Monoid' m where 
    midentity' :: Identity a -> m a 
    mappend' :: (m <+> m) a -> m a 

này desugars để

midentity' :: a -> m a 
mappend' :: m (m a) -> m a 

Look quen thuộc?

+0

aah, Monad là endofuctor, làm cách nào tôi bỏ lỡ điều đó. Giờ thì rõ ràng, cảm ơn. –

5

Định nghĩa "Monads chỉ là monoids trong danh mục endofunctors.", Mặc dù đúng là một nơi tồi tệ để bắt đầu. Đó là từ một số blog post được dự định là trò đùa. Nhưng nếu bạn quan tâm đến sự tương ứng, nó có thể được thể hiện trong Haskell:

Mô tả laymen của một thể loại là một bộ sưu tập trừu tượng các đối tượng và hình thái giữa các đối tượng. Ánh xạ giữa các danh mục được gọi là functors và các đối tượng bản đồ cho các đối tượng và hình thái đối với hình thái liên quan và bảo tồn danh tính. An endofunctor là một hàm từ một danh mục cho chính nó.

{-# LANGUAGE MultiParamTypeClasses, 
      ConstraintKinds, 
      FlexibleInstances, 
      FlexibleContexts #-} 

class Category c where 
    id :: c x x 
    (.) :: c y z -> c x y -> c x z 

class (Category c, Category d) => Functor c d t where 
    fmap :: c a b -> d (t a) (t b) 

type Endofunctor c f = Functor c c f 

Mappings giữa functors đáp ứng cái gọi là naturality conditions được gọi là biến đổi tự nhiên. Trong Haskell đây là những chức năng đa hình của loại: (Functor f, Functor g) => forall a. f a -> g a.

Một đơn nguyên trên một loại C là ba điều (T,η,μ), T là endofunctor và 1 là functor nhận dạng trên C. Mu và eta là hai biến đổi tự nhiên mà đáp ứng một bản sắc triangle identity và một associativity, và được định nghĩa là:

  • η : 1 → T
  • μ : T^2 → T

Trong Haskell μjoinηreturn

  • return :: Monad m => a -> m a
  • join :: Monad m => m (m a) -> m a

Một định nghĩa phân loại của Monad trong Haskell có thể được viết:

class (Endofunctor c t) => Monad c t where 
    eta :: c a (t a) 
    mu :: c (t (t a)) (t a) 

Nhà điều hành ràng buộc có thể được bắt nguồn từ những.

(>>=) :: (Monad c t) => c a (t b) -> c (t a) (t b) 
(>>=) f = mu . fmap f 

Đây là một định nghĩa đầy đủ, nhưng tương đương bạn cũng có thể cho thấy rằng luật Monad có thể được diễn tả như luật monoid với một loại functor. Chúng ta có thể xây dựng thể loại functor này là một thể loại với các đối tượng như functors (tức là ánh xạ giữa các loại) và các phép biến đổi tự nhiên (tức là ánh xạ giữa các functors) như là các hình thái. Trong một thể loại của endofunctors tất cả các functors là functors giữa cùng một loại.

newtype CatFunctor c t a b = CatFunctor (c (t a) (t b)) 

Chúng tôi có thể hiển thị này làm phát sinh một loại với thành phần functor như thành phần cấu xạ:

-- Note needs UndecidableInstances to typecheck 
instance (Endofunctor c t) => Category (CatFunctor c t) where 
    id = CatFunctor id 
    (CatFunctor g) . (CatFunctor f) = CatFunctor (g . f) 

Các monoid có định nghĩa thông thường:

class Monoid m where 
    unit :: m 
    mult :: m -> m -> m 

Một monoid trên một danh mục của functors có một biến đổi tự nhiên như là một bản sắc và một phép toán nhân kết hợp các biến đổi tự nhiên. Thành phần Kleisli có thể được định nghĩa để thỏa mãn luật nhân.

(<=<) :: (Monad c t) => c y (t z) -> c x (t y) -> c x (t z) 
f <=< g = mu . fmap f . g 

Và như vậy bạn có nó "Monads chỉ monoids trong danh mục của endofunctors" mà chỉ là một "pointfree" phiên bản của định nghĩa bình thường của monads từ endofunctors và (mu, eta).

instance (Monad c t) => Monoid (c a (t a)) where 
    unit = eta 
    mult = (<=<) 

Với một chút thay ai có thể chứng minh rằng các đặc tính của monoidal (<=<) Are tuyên bố tương đương của tam giác và associativity sơ đồ cho biến đổi tự nhiên của đơn nguyên.

f <=< unit == f 
unit <=< f == f 

f <=< (g <=< h) == (f <=< g) <=< h 

Nếu bạn quan tâm đến diagrammatic representations Tôi đã viết một chút về việc thể hiện chúng bằng sơ đồ chuỗi.

2

Dường như với tôi rằng bạn bỏ qua điều quan trọng:

  • Có chữ “monoid” trong định nghĩa. Bạn đã không xem xét nó trong bài viết của bạn.
  • Tốt hơn nên thay thế bằng “vật thể đơn” để chính xác. Monoids sống trong đại số trừu tượng, đối tượng monoid sống trong lý thuyết thể loại. Loài khác nhau.
    • Monoids là các đối tượng đơn lẻ trong một số danh mục, nhưng điều này không liên quan ở đây.
  • Đối tượng monoid chỉ có thể được xác định trong danh mục monoidal.

Vì vậy, đường dẫn để hiểu định nghĩa như sau.

  • Bạn hãy xem xét một chủng loại endofunctors (cho phép gọi nó là E) trên chủng loại loại Haskell và chức năng Hask. Các đối tượng của nó là các functors trên Hask, một hình thái trong đó từ F đến G là một hàm đa hình của loại F a -> G a với một số thuộc tính.
  • Bạn xem xét một cấu trúc trên E biến nó thành một thể loại monoidal, tức là thành phần của các functors và các functors danh tính.
  • Bạn xem xét định nghĩa của một đối tượng monoid, ví dụ: từ Wikipedia.
  • Bạn xem xét ý nghĩa của nó trong danh mục cụ thể của bạn E. Nó có nghĩa là M là một endofunctor, và μ có cùng kiểu như “join”, và η có cùng kiểu như “return”.
  • “(>> =)” được xác định qua “tham gia”.

Lời khuyên. Đừng cố gắng thể hiện mọi thứ trong Haskell. Nó được thiết kế để viết chương trình, chứ không phải toán học. Ký hiệu toán học là thuận tiện hơn ở đây bởi vì bạn có thể viết thành phần của functors là “∘” mà không gặp rắc rối với trình kiểm tra kiểu.

Các vấn đề liên quan