Bài 4: 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ả, 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ử người đó alice muốn mua một con mèo của bob, nhưng cả hai đều không tin người kia. May mắn thay, họ có một người bạn chung carol mà cả hai đều tin tưởng là trung lập (nhưng không đủ để đưa cho cô ấy tiền và 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 When có 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 dự định của điều này là khi thực thi 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, When cung cấp một danh sách các trường hợp, mỗi trường hợp có một thực thi và một hợp đồng tương ứng được kích hoạt khi thực thi đó xảy ra. Sử dụng điều này, chúng ta có thể cho phép tùy chọn bob đưa ra lựa chọn đầu tiên, thay vì alice như 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 ta sẽ hoàn nguyên về phiên bản đơn giản hơn ở phần alice chọn đầu tiên.
- 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 ta đã giả định rằng Alice đã cam kết thanh toán của mình, nhưng giả sử rằng chúng ta muốn thiết kế một hợp đồng để đảm bảo rằng: chúng ta 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. Mỗi lần chúng ta thấy a When, chúng ta cần cung cấp hai điều bổ sung:
- Thời gian chờ sau đó hợp đồng sẽ tiến triển, và
- Hợp đồng tiếp tục mà nó tiến triển.
Thêm Thời gian chờ vào hợp đồng
Trước 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 When không bao giờ trở thành sự thật. Vì vậy, chúng ta thêm các giá trị thời gian chờ và tiếp tục cho mỗi giá trị When xảy ra trong hợp đồng.
When [ Case aliceChoice
(When [ Case bobChoice
(If (aliceChosen ValueEQ bobChosen)
agreement
arbitrate) ]
60 *-- ADDED*
arbitrate) *-- ADDED*
]
40 *-- ADDED*
Close *-- ADDED*
Điểm 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 theo slot 40, hợp đồng sẽ bị đóng và tất cả số tiền trong hợp đồng sẽ được hoàn trả.
Close thườ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 ta sẽ mô tả điều này chi tiết hơn khi chúng ta 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, hoàn trả sẽ xảy ra ở số slot 40.
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 ta chờ đợi một cấu trúc từ Bob. Nếu điều đó không xảy ra theo thời gian 60, thì Carol sẽ được kêu gọi để phân xử. [2]
Thêm Cam kết vào hợp đồng
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) ]
60
arbitrate)
]
40
Close)
]
10 *-- 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ờ ở số slot 10 khi thực hiện 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, agreement và, sử dụng nhúng price Haskell của Marlowe DSL để đưa ra một số định nghĩa viết tắt. chúng ta cũng sử dụng các chuỗi quá tải để làm cho một số mô tả - ví dụ về tài khoản - ngắn gọn hơ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.
- 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ờ 40 của
Whenđược thay thế bằng60và ngược lại? Có hợp lý không nếu có cùng một khoảng thời gian chờ, 100 chẳng hạn như trên mỗi nhómWhen? 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 hướng dẫn tiếp theo, chúng ta sẽ trình bày ngôn ngữ đầy đủ.
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ò (Role) 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.
