Một số câu hỏi về các monads trong Haskell

Question

Tôi đang tìm hiểu về các monads và có một vài câu hỏi.

Đây là nơi tôi đang ở ngay bây giờ. Xin vui lòng sửa tôi, nơi tôi sai.

• Biểu tượng >>= là một toán tử kết hợp. Các toán tử Infix là các hàm lấy hai đối số (bên trái và bên phải) và trả về một giá trị.

• Biểu tượng >>= được gọi là toán tử liên kết và có chữ ký Monad m => m t -> (t -> m u) -> m u. Tuy nhiên, các loại dường như không xếp hàng ở đây. Chúng tôi nhận được một giá trị loại m t và đối số thứ hai là một hàm mất t. (Tôi không thấy làm thế nào để kết nối các dấu chấm.)

• này phải có nghĩa là chức năng ràng buộc là bằng cách nào đó có khả năng loại bỏ các m từ m t để có được t và vượt qua nó để hàm.

Dưới đây là những câu hỏi của tôi:

• là khả năng loại bỏ các m từ m t cái gì mà chỉ có thể bên trong một nhà điều hành ràng buộc như vậy. Nhà điều hành liên kết này có một số đặc quyền riêng hay gì đó không?

• Nó phải làm gì với các thay đổi trạng thái? Tôi hiểu (tôi nghĩ) rằng mục đích của các monads là 'quấn' các tác dụng phụ để chúng được phân lập khỏi phần còn lại của chương trình. Nhưng vai trò của nhà điều hành liên kết trong điều này là gì?

Answer 1

Khả năng xóa 'M' khỏi 'M t' có thể chỉ có thể thực hiện được bên trong toán tử liên kết như vậy. Nhà điều hành liên kết này có một số đặc quyền riêng hay gì đó không?

Ràng buộc không theo bất kỳ trường hợp đặc biệt nào, nhưng thường thì nó sẽ được định nghĩa trong cùng một mô-đun như kiểu dữ liệu monads. Do đó, nó có thể biết về (và sử dụng) các chi tiết không được mô-đun xuất ra. Trường hợp thông thường sẽ là module xuất ra một kiểu dữ liệu, nhưng không phải là các hàm tạo hoặc các chi tiết khác về các kiểu cấu trúc bên trong. Sau đó, đối với mã sử dụng mô-đun, các hoạt động bên trong của kiểu dữ liệu là vô hình và mã đó không thể trực tiếp sửa đổi các giá trị của loại này.

Trái với các chức năng được xác định bên trong mô-đun, ví dụ như một số toán tử liên kết >>=, có thể truy cập bất kỳ thứ gì chúng thích từ mô-đun được xác định.

Trường hợp đặc biệt là IO đơn nguyên, vì nó không được định nghĩa bởi một mô-đun, nhưng được tích hợp vào hệ thống/trình biên dịch thời gian chạy. Ở đây trình biên dịch biết về các chi tiết bên trong của nó thực hiện và cho thấy các hàm như >>= của IO. Việc triển khai các chức năng này thực sự được đặc quyền đặc biệt vì chúng sống "bên ngoài chương trình", nhưng đây là trường hợp đặc biệt và thực tế này không nên quan sát được từ bên trong Haskell.

Nó phải làm gì với các thay đổi trạng thái? Tôi hiểu (tôi nghĩ) rằng mục đích của các monads là 'quấn' các tác dụng phụ để chúng được phân lập khỏi phần còn lại của chương trình. Nhưng vai trò của nhà điều hành liên kết trong điều này là gì?

Nó không thực sự cần phải làm gì với các thay đổi trạng thái, đây chỉ là một vấn đề có thể được xử lý với moands. Các đơn vị IO được sử dụng để có IO thực hiện theo một thứ tự nhất định, nhưng nói chung monads chỉ là cách kết hợp các chức năng với nhau.

Thông thường, một đơn nguyên (cụ thể là hàm liên kết) xác định cách thức mà các chức năng nhất định sẽ được tạo thành cùng nhau thành các hàm lớn hơn. Phương pháp kết hợp các hàm này được tóm tắt trong đơn nguyên. Chính xác việc kết hợp này hoạt động như thế nào hoặc tại sao bạn muốn kết hợp các hàm theo cách như vậy không quan trọng, một đơn nguyên chỉ định một cách kết hợp các hàm nhất định theo một cách nhất định. (Xem thêm this "Monads for C# programmers" answer nơi tôi về cơ bản lặp lại một vài lần với các ví dụ.)

Answer 2

là khả năng loại bỏ các 'M' từ 'M t' cái gì mà chỉ có thể bên trong một nhà điều hành ràng buộc như vậy.

Vâng, đó là chắc chắn có thể bên trong các nhà điều hành ràng buộc, as type của nó quy định cụ thể:

(>>=) :: m a -> (a -> m b) -> m b 

Chức năng 'chạy' cho đơn nguyên của bạn thường có thể làm được điều này cũng (để trả về một giá trị tinh khiết từ tính toán của bạn).

mục tiêu monads là 'quấn' tác dụng phụ do đó họ đang bị cô lập với phần còn lại của chương trình

Hmm. Không, monads cho phép chúng ta mô hình hóa khái niệm tính toán. Các tính toán tác dụng phụ chỉ là một khái niệm như vậy, như trạng thái, backtracking, continuations, concurrency, transaction, kết quả tùy chọn, kết quả ngẫu nhiên, trạng thái có thể hoàn nguyên, không xác định ... tất cả đều là can be described as a monad

Đơn nguyên IO là gì bạn đang đề cập đến, tôi giả định. Nó là một đơn lẻ hơi kỳ quặc - nó tạo ra chuỗi các thay đổi trừu tượng đối với trạng thái của thế giới, sau đó được đánh giá bởi thời gian chạy. Ràng buộc chỉ cho phép chúng ta sắp xếp thứ tự theo thứ tự đúng trong trình đơn IO - và trình biên dịch sau đó sẽ dịch tất cả các hành động sửa đổi thế giới theo thứ tự này thành mã bắt buộc làm thay đổi trạng thái của máy.

Điều đó rất cụ thể đối với đơn nguyên IO mặc dù không phải là monads nói chung.

Answer 3

Tôi rất khuyên bạn nên đọc (http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html). Nó cho một lý do hoàn hảo, thông thường lý do tại sao monads tồn tại.

Answer 4

Sau đây là định nghĩa của loại lớp Monad.

class Monad m where 

    (>>=)  :: forall a b. m a -> (a -> m b) -> m b 
    (>>)  :: forall a b. m a -> m b -> m b 
    return  :: a -> m a 
    fail  :: String -> m a 

    m >> k  = m >>= \_ -> k 
    fail s  = error s 

Mỗi loại kiểu loại Monad xác định chức năng riêng của mình >>=.Dưới đây là một ví dụ từ loại thẩm Maybe:

instance Monad Maybe where 

    (Just x) >>= k  = k x 
    Nothing >>= _  = Nothing 

    (Just _) >> k  = k 
    Nothing >> _  = Nothing 

    return    = Just 
    fail _    = Nothing 

Như chúng ta có thể thấy, vì phiên bản Maybe của >>= được đặc biệt được xác định để hiểu được Maybe loại sơ thẩm, và bởi vì nó được quy định tại một nơi mà có quyền truy cập hợp pháp vào các nhà xây dựng dữ liệu data Maybe a dữ liệu Nothing và Just a, phiên bản Maybe của >>= có thể bỏ qua số a trong số Maybe a và chuyển chúng qua.

Để làm việc thông qua một ví dụ, chúng ta có thể thực hiện:

x :: Maybe Integer 
x = do a <- Just 5 
     b <- Just (a + 1) 
     return b 

De-sugared, làm-ký hiệu trở thành:

x :: Maybe Integer 
x = Just 5  >>= \a -> 
    Just (a + 1) >>= \b -> 
    Just b 

Những đánh giá như:

=     (\a -> 
    Just (a + 1) >>= \b -> 
    Just b) 5 

    = Just (5 + 1) >>= \b -> 
    Just b 

    =     (\b -> 
    Just b) (5 + 1) 

    = Just (5 + 1) 

    = Just 6 

Answer 5

Các các loại xếp hàng, vui vẻ đủ. Đây là cách làm.

Hãy nhớ rằng một đơn nguyên cũng là một hàm. Hàm sau đây được định nghĩa cho tất cả các functors:

fmap :: (Functor f) => (a -> b) -> f a -> f b 

Bây giờ câu hỏi: Các loại này thực sự xếp hàng? Vâng, vâng. Với chức năng từ a đến b, thì nếu chúng ta có một môi trường f, trong đó a có sẵn, chúng tôi có một môi trường f trong đó có b.

Bằng cách tương tự với tam đoạn luận:

(Functor Socrates) => (Man -> Mortal) -> Socrates Man -> Socrates Mortal 

Bây giờ, như bạn đã biết, một đơn nguyên là một functor trang bị ràng buộc và trả lại:

return :: (Monad m) => a -> m a 
(=<<) :: (Monad m) => (a -> m b) -> m a -> m b 

Bạn không thể biết rằng tương đương, đó là một functor được trang bị trả lại và tham gia:

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

Xem cách chúng tôi đang xóa một số m. Với một đơn nguyên m, bạn không thể luôn nhận được từ m a đến a, nhưng bạn luôn có thể nhận được từ m (m a) đến m a.

Bây giờ, hãy xem đối số đầu tiên là . Đó là một chức năng của loại (a -> m b). Điều gì xảy ra khi bạn chuyển hàm đó tới fmap? Bạn nhận được m a -> m (m b). Vì vậy, "lập bản đồ" trên một số m a với chức năng a -> m b cung cấp cho bạn m (m b). Lưu ý rằng đây chính là kiểu đối số cho join. Đây không phải là một trùng hợp ngẫu nhiên.Một thực hiện hợp lý "ràng buộc" trông như thế này:

(>>=) :: m a -> (a -> m b) -> m b 
x >>= f = join (fmap f x) 

Trong thực tế, ràng buộc và tham gia có thể được xác định theo nhau:

join = (>>= id) 

Answer 6

Tôi hiểu (tôi nghĩ) rằng mục tiêu của monads là 'quấn' các tác dụng phụ để chúng được phân lập từ phần còn lại của chương trình.

Thực tế nó hơi tinh tế hơn thế. Monads cho phép chúng ta lập mô hình trình tự theo cách rất chung chung. Thường thì khi bạn nói chuyện với một chuyên gia tên miền, bạn thấy họ nói một cái gì đó như "đầu tiên chúng tôi thử X. Sau đó, chúng tôi thử Y, và nếu điều đó không làm việc thì chúng tôi thử Z". Khi bạn đến để thực hiện một cái gì đó như thế trong một ngôn ngữ thông thường bạn thấy rằng nó không phù hợp, vì vậy bạn phải viết rất nhiều mã phụ để trang trải bất cứ điều gì chuyên gia miền có nghĩa là bởi từ "sau đó".

Trong Haskell, bạn có thể thực hiện điều này dưới dạng đơn vị có "sau đó" được dịch sang toán tử liên kết. Vì vậy, ví dụ tôi đã từng viết một chương trình mà một mục phải được chỉ định từ các hồ bơi theo các quy tắc nhất định. Đối với trường hợp 1 bạn lấy nó từ hồ bơi X. Nếu đó là sản phẩm nào sau đó bạn chuyển sang hồ Y. Đối với trường hợp 2 bạn phải lấy nó trực tiếp từ hồ Y. Và như vậy cho một tá hoặc trường hợp, bao gồm một số nơi bạn đã ít nhất gần đây được sử dụng từ cả hai nhóm X hoặc Y. Tôi đã viết một đơn nguyên tùy chỉnh đặc biệt cho công việc đó để tôi có thể viết:

case c of 
    1: do {try poolX; try poolY} 
    2: try poolY 
    3: try $ lru [poolX, poolY] 

Nó hoạt động rất tốt.

Tất nhiên điều này bao gồm các mô hình chuỗi thông thường. Đơn nguyên IO là mô hình mà tất cả các ngôn ngữ lập trình khác có; nó chỉ trong Haskell một sự lựa chọn rõ ràng hơn là một phần của môi trường. ST monad cung cấp cho bạn đột biến bộ nhớ của IO, nhưng không có đầu vào và đầu ra thực tế. Mặt khác, đơn vị trạng thái cho phép bạn giới hạn trạng thái của mình thành một giá trị duy nhất của một loại được đặt tên.

Đối với một cái gì đó thực sự bị bẻ cong não, hãy xem this blog post về một đơn vị trạng thái lạc hậu. Nhà nước tuyên truyền theo hướng ngược lại với "thực thi". Nếu bạn nghĩ về điều này giống như một đơn vị nhà nước thực hiện một lệnh theo sau là tiếp theo, sau đó một "đặt" sẽ gửi giá trị trạng thái ngược thời gian tới bất kỳ tiền tố "nhận" nào. Điều gì thực sự là xảy ra là một chức năng đệ quy lẫn nhau được thiết lập mà chỉ chấm dứt nếu không có nghịch lý. Tôi không hoàn toàn chắc chắn nơi để sử dụng một monad như vậy, nhưng nó minh họa quan điểm về monads là mô hình tính toán.

Nếu bạn chưa sẵn sàng cho điều đó, thì chỉ cần nghĩ đến liên kết dưới dạng dấu chấm phẩy quá tải. Điều đó giúp bạn có được một chặng đường dài.