Skip to content

Commit

Permalink
Fix & simplify SOP encoding example comment (#6231)
Browse files Browse the repository at this point in the history
Here's a small fix for the comment:

- use one variable for the type everywhere
- fix ordering of `constr` arguments

Additionally,

- align the corresponding parts in the text
  • Loading branch information
klntsky authored and effectfully committed Aug 6, 2024
1 parent d134840 commit 3df4939
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions plutus-core/plutus-ir/src/PlutusIR/Compiler/Datatype.hs
Original file line number Diff line number Diff line change
Expand Up @@ -185,17 +185,17 @@ We still need to think about the types. In general, we need:
For example, consider 'data Maybe a = Nothing | Just a'. Then:
- The type corresponding to the datatype is:
Maybe = \(t :: *) . sop [] [a]
Maybe = \(a :: *) . sop [] [a]
- The type of the constructors are:
Just : forall (t :: *) . a -> Maybe a
Nothing : forall (t :: *) . Maybe a
Nothing : forall (a :: *) . Maybe a
Just : forall (a :: *) . a -> Maybe a
- The terms for the constructors are:
Just = /\(t :: *) \(x :: t) . constr (Maybe t) 1 x
Nothing = /\(t :: *) . constr 0 (Maybe t)
Nothing = /\(a :: *) . constr 0 (Maybe a)
Just = /\(a :: *) \(x :: a) . constr 1 (Maybe a) x
- The type of the destructor is:
match_Maybe :: forall (t :: *) . Maybe t -> forall (out_Maybe :: *) . out_Maybe -> (t -> out_Maybe) -> out_Maybe
match_Maybe :: forall (a :: *) . Maybe a -> forall (out_Maybe :: *) . out_Maybe -> (a -> out_Maybe) -> out_Maybe
- The term for the destructor is:
match_Maybe = /\(t :: *) \(x : Maybe t) /\(out_Maybe :: *) \(case_Nothing :: out_Maybe) (case_Just :: t -> out_Maybe) .
match_Maybe = /\(a :: *) \(x : Maybe a) /\(out_Maybe :: *) \(case_Nothing :: out_Maybe) (case_Just :: a -> out_Maybe) .
case out_Maybe x case_Nothing case_Just
-- General case
Expand Down

0 comments on commit 3df4939

Please sign in to comment.