From aca3bba91873c37c73b1a296fd6920cbc54ebb0d Mon Sep 17 00:00:00 2001 From: Vladimir Kalnitsky Date: Fri, 21 Jun 2024 14:19:03 +0400 Subject: [PATCH] Fix & simplify SOP encoding example comment --- .../plutus-ir/src/PlutusIR/Compiler/Datatype.hs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Datatype.hs b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Datatype.hs index 8015fe8a349..9f8e28c9c6b 100644 --- a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Datatype.hs +++ b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Datatype.hs @@ -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