Ví dụ đầu tiên

Hướng dẫn này giới thiệu một hợp đồng tài chính đơn giản trong mã giả (pseudocode), trước khi giải thích cách nó được sửa đổi để hoạt động trong Marlowe, đưa ra ví dụ đầu tiên về hợp đồng Marlowe.

Một hợp đồng ký quỹ đơn giản

Giả sử alice muốn mua một con mèo của bob, nhưng cả hai đều không tin tưởng người kia. May mắn thay, họ có một người bạn chung carol mà cả hai đều tin tưởng trung lập (nhưng không đủ tin cậy để đưa tiền và cho cô ấy làm trung gian). Do đó, họ đồng ý về hợp đồng sau, được viết bằng mã giả chức năng đơn giản. Loại hợp đồng này là một ví dụ đơn giản về ký quỹ .

When aliceChoice
     (When bobChoice
           (If (aliceChosen `ValueEQ` bobChosen)
               agreement
               arbitrate))

Hợp đồng được mô tả bằng cách sử dụng các hàm tạo của kiểu dữ liệu Haskell. Hàm tạo ngoài cùng Whencó hai đối số: đối số đầu tiên là một quan sát và đối số thứ hai là một hợp đồng khác. Ý nghĩa của điều này là khi hành động xảy ra, hợp đồng thứ hai được kích hoạt.

Bản thân hợp đồng thứ hai là một hợp đồng khác When- yêu cầu một quyết định từ bob- nhưng bên trong đó, có một sự lựa chọn : If alice và bobđồng ý về những gì phải làm, nó được thực hiện; nếu không, carolđược yêu cầu phân xử và đưa ra quyết định.

Nói chung, Whencung cấp một danh sách các trường hợp , mỗi trường hợp có một hành động và một hợp đồng tương ứng được kích hoạt khi hành động đó xảy ra. Sử dụng điều này, chúng tôi có thể cho phép tùy chọn bobđưa ra lựa chọn đầu tiên, thay vì alicenhư thế này:

When [ Case aliceChoice
            (When [ Case bobChoice
                        (If (aliceChosen `ValueEQ` bobChosen)
                           agreement
                           arbitrate) ],
       Case bobChoice
            (When [ Case aliceChoice
                        (If (aliceChosen `ValueEQ` bobChosen)
                            agreement
                            arbitrate) ]
     ]

Trong hợp đồng này, Alice hoặc Bob có thể đưa ra lựa chọn đầu tiên; người kia sau đó đưa ra lựa chọn. Nếu họ đồng ý, thì điều đó được thực hiện; nếu không, Carol phân xử. Trong phần còn lại của hướng dẫn, chúng tôi sẽ hoàn nguyên về phiên bản đơn giản hơn ở phần alicechọn đầu tiên.

Bài tập

Hãy suy nghĩ về việc thực hiện hợp đồng này trong thực tế. Giả sử rằng Alice đã cam kết một số tiền cho hợp đồng. Điều gì sẽ xảy ra nếu Bob chọn không tham gia nữa?

Chúng tôi đã giả định rằng Alice đã cam kết thanh toán của mình, nhưng giả sử rằng chúng tôi muốn thiết kế một hợp đồng để đảm bảo rằng: chúng tôi cần phải làm gì?

Ký quỹ tại Marlowe

Các hợp đồng Marlowe kết hợp các cấu trúc bổ sung để đảm bảo rằng chúng tiến triển đúng cách. Mỗi lần chúng tôi thấy hàm When, chúng tôi cần cung cấp hai điều bổ sung:

  • thời gian chờ (timeout) mà sau đó hợp đồng sẽ tiến triển, và

  • hợp đồng tiếp tục (continuation) mà nó triển khai.

Thêm thời gian chờ

Đầu tiên, chúng ta hãy kiểm tra cách sửa đổi những gì chúng ta đã viết để đề phòng trường hợp điều kiện Whenkhông bao giờ trở thành sự thật. Vì vậy, chúng tôi thêm giá trị thời gian chờ và giá trị tiếp tục cho từng giá trị Whenxảy ra trong hợp đồng.

When [ Case aliceChoice
            (When [ Case bobChoice
                        (If (aliceChosen `ValueEQ` bobChosen)
                           agreement
                           arbitrate) ]
                  1700007200    -- ADDED
                  arbitrate)    -- ADDED
      ]
      1700003600   -- ADDED
      Close        -- ADDED

Ngoài cùng When, yêu cầu Alice thực hiện lựa chọn đầu tiên: nếu Alice không đưa ra lựa chọn trước giờ POSIX 1700003600(2023-11-14 23:13:20 GMT), hợp đồng sẽ bị đóng và tất cả số tiền trong hợp đồng sẽ được hoàn trả .

Closethường là bước cuối cùng trong mọi “con đường” thông qua hợp đồng Marlowe và tác dụng của nó là hoàn trả số tiền trong hợp đồng cho những người tham gia; chúng tôi sẽ mô tả điều này chi tiết hơn khi chúng tôi xem xét từng bước của Marlowe trong hướng dẫn sau. Trong trường hợp cụ thể này, việc hoàn tiền sẽ xảy ra vào lúc POSIX 1700003600(2023-11-14 23:13:20 GMT).

Nhìn vào các cấu trúc bên trong, nếu lựa chọn của Alice đã được thực hiện, thì chúng tôi chờ đợi một cấu trúc từ Bob. Nếu điều đó không xảy ra trước thời điểm POSIX 1700007200(2023-11-15 00:13:20 GMT), thì Carol sẽ được yêu cầu phân xử. 2

Thêm cam kết

Tiếp theo, chúng ta nên xem xét tiền mặt được cam kết như thế nào trong bước đầu tiên của hợp đồng.

When [Case (Deposit "alice" "alice" ada price)   -- ADDED
 (When [ Case aliceChoice
             (When [ Case bobChoice
                         (If (aliceChosen `ValueEQ` bobChosen)
                            agreement
                            arbitrate) ]
                   1700007200
                   arbitrate)
       ]
       1700003600
       Close)
   ]
   1700000000                              -- ADDED
   Close                                   -- ADDED

Một khoản tiền gửi priceđược yêu cầu từ "alice": nếu nó được trao, thì nó được giữ trong một tài khoản, còn được gọi là "alice". Các tài khoản như thế này chỉ tồn tại trong thời hạn của hợp đồng; mỗi tài khoản thuộc về một hợp đồng duy nhất.

Có một khoảng thời gian chờ tại thời điểm POSIX 1700000000(2023-11-14 22:13:20 GMT) khi gửi tiền; Nếu đạt được điều đó mà không đặt cọc, hợp đồng sẽ được đóng và tất cả số tiền đã có trong hợp đồng sẽ được hoàn trả. Trong trường hợp này, đó chỉ đơn giản là kết thúc hợp đồng.

Định nghĩa

Chúng ta sẽ thấy ở phần sau của mô tả hợp đồng này, chẳng hạn như arbitrate, agreementvà price, sử dụng nhúng Haskell của Marlowe DSL để đưa ra một số định nghĩa viết tắt. Chúng tôi cũng sử dụng các chuỗi quá tải (overloaded) để làm cho một số mô tả - ví dụ về tài khoản.

Những điều này sẽ được thảo luận chi tiết hơn khi chúng ta xem xét Marlowe được nhúng trong Haskell .

Bài tập

Nhận xét về lựa chọn giá trị thời gian chờ và xem xét các lựa chọn thay thế.

Ví dụ: điều gì sẽ xảy ra nếu thời gian chờ 1700003600 (2023-11-14 23:13:20 GMT) Whenđược thay thế bằng 1700007200(2023-11-15 00:13:20 GMT) và ngược lại? Có hợp lý không nếu có cùng một khoảng thời gian chờ 1700010800 (2023-11-15 01:13:20 GMT), cho mỗi thứ When? Nếu không, tại sao không?

Ví dụ này đã chỉ ra nhiều thành phần của ngôn ngữ hợp đồng Marlowe; trong phần hướng dẫn tiếp theo, chúng tôi sẽ trình bày đầy đủ về ngôn ngữ này.

Ghi chú

  • Mặc dù tên của Alice, Bob, v.v. được “gắn chặt” vào hợp đồng ở đây, chúng ta sẽ thấy sau này rằng những tên này có thể được thể hiện bằng các vai trò trong tài khoản, chẳng hạn như người mua và người bán . Những vai trò này sau đó có thể được liên kết với những người tham gia cụ thể khi một hợp đồng được chạy; chúng ta sẽ thảo luận thêm về vấn đề này trong phần tiếp theo.

Lý lịch

Những công bố này bao gồm công việc ban đầu về việc sử dụng lập trình chức năng để mô tả các hợp đồng tài chính.

1

Danh sách trong Marlowe được bao gồm trong dấu ngoặc vuông, như trong [2,3,4].

2

Một lần nữa, chúng tôi sẽ mô tả cách thức arbitratevà agreementhoạt động của Marlowe được nhúng .

PreviousGiới thiệu MarloweNextMô hình Marlowe

Last updated