[Builtin] Define 'caseList' in terms of 'chooseList'

plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/List.hs

@@ -8,6 +8,7 @@ module PlutusCore.StdLib.Data.List
     ( list
     , caseList
     , foldrList
+    , foldList
     ) where
 
 import           PlutusCore.Core
@@ -16,7 +17,6 @@ import           PlutusCore.MkPlc
 import           PlutusCore.Name
 import           PlutusCore.Quote
 
-import           PlutusCore.StdLib.Data.Bool
 import           PlutusCore.StdLib.Data.Function
 import           PlutusCore.StdLib.Data.Unit
 
@@ -29,11 +29,13 @@ list = mkTyBuiltin @_ @[] ()
 -- equivalent to @unwrap xs@ on lists defined in PLC itself (hence why we bind @r@ after @xs@).
 --
 -- > /\(a :: *) -> \(xs : list a) -> /\(r :: *) -> (z : r) (f : a -> list a -> r) ->
--- >     ifThenElse
--- >         {r}
--- >         (Null {a} xs)
+-- >     chooseList
+-- >         {a}
+-- >         {() -> r}
+-- >         xs
 -- >         (\(u : ()) -> z)
 -- >         (\(u : ()) -> f (head {a} xs) (tail {a} xs))
+-- >         ()
 caseList :: TermLike term TyName Name DefaultUni DefaultFun => term ()
 caseList = runQuote $ do
     a <- freshTyName "a"
@@ -50,10 +52,15 @@ caseList = runQuote $ do
         . tyAbs () r (Type ())
         . lamAbs () z (TyVar () r)
         . lamAbs () f (TyFun () (TyVar () a) . TyFun () listA $ TyVar () r)
-        $ mkIterApp () (tyInst () ifThenElse $ TyVar () r)
-            [ funAtXs NullList
+        $ mkIterApp ()
+                (mkIterInst () (builtin () ChooseList)
+                    [ TyVar () a
+                    , TyFun () unit $ TyVar () r
+                    ])
+            [ var () xs
             , lamAbs () u unit $ var () z
             , lamAbs () u unit $ mkIterApp () (var () f) [funAtXs HeadList, funAtXs TailList]
+            , unitval
             ]
 
 -- |  @foldr@ over built-in lists.
@@ -89,3 +96,36 @@ foldrList = runQuote $ do
             [ var () x
             , apply () (var () rec) $ var () xs'
             ]
+
+-- |  'foldl\'' as a PLC term.
+--
+-- > /\(a :: *) (r :: *) -> \(f : r -> a -> r) ->
+-- >     fix {r} {list a -> r} \(rec : r -> list a -> r) (z : r) (xs : list a) ->
+-- >         caseList {a} xs {r} z \(x : a) (xs' : list a) -> rec (f z x) xs'
+foldList :: TermLike term TyName Name DefaultUni DefaultFun => term ()
+foldList = runQuote $ do
+    a   <- freshTyName "a"
+    r   <- freshTyName "r"
+    f   <- freshName "f"
+    rec <- freshName "rec"
+    z   <- freshName "z"
+    xs  <- freshName "xs"
+    x   <- freshName "x"
+    xs' <- freshName "xs'"
+    let listA = TyApp () list $ TyVar () a
+        unwrap' ann = apply ann . tyInst () caseList $ TyVar () a
+    return
+        . tyAbs () a (Type ())
+        . tyAbs () r (Type ())
+        . lamAbs () f (TyFun () (TyVar () r) . TyFun () (TyVar () a) $ TyVar () r)
+        . apply () (mkIterInst () fix [TyVar () r, TyFun () listA $ TyVar () r])
+        . lamAbs () rec (TyFun () (TyVar () r) . TyFun () listA $ TyVar () r)
+        . lamAbs () z (TyVar () r)
+        . lamAbs () xs listA
+        . apply () (apply () (tyInst () (unwrap' () (var () xs)) $ TyVar () r) $ var () z)
+        . lamAbs () x (TyVar () a)
+        . lamAbs () xs' listA
+        . mkIterApp () (var () rec)
+        $ [ mkIterApp () (var () f) [var () z, var () x]
+          , var () xs'
+          ]

plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Everything.hs

@@ -66,6 +66,7 @@ stdLib =
                   [ plcTypeFile "List"      list
                   , plcTermFile "CaseList"  Builtin.caseList
                   , plcTermFile "FoldrList" Builtin.foldrList
+                  , plcTermFile "FoldList"  Builtin.foldList
                   ]
               , treeFolderContents "Data"
                   [ plcTypeFile "Data"     dataTy

plutus-core/plutus-core/test/Pretty/Golden/Readable/Examples/Data/ofoldrData.plc.golden

@@ -1 +1 @@
-\(fConstr : integer -> list data -> data) -> \(fMap : list (pair data data) -> data) -> \(fList : list data -> data) -> \(fI : integer -> data) -> \(fB : bytestring -> data) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {data} {data} (\(rec : data -> data) -> \(d : data) -> (\(d : data) -> /\(r :: *) -> \(fConstr : integer -> list (data) -> r) -> \(fMap : list (pair (data) (data)) -> r) -> \(fList : list (data) -> r) -> \(fI : integer -> r) -> \(fB : bytestring -> r) -> (Left chooseData) {unit -> r} d (\(u : unit) -> (/\(a :: *) -> /\(b :: *) -> /\(c :: *) -> \(f : a -> b -> c) -> \(p : pair a b) -> f ((Left fstPair) {a} {b} p) ((Left sndPair) {a} {b} p)) {integer} {list (data)} {r} fConstr ((Left unConstrData) d)) (\(u : unit) -> fMap ((Left unMapData) d)) (\(u : unit) -> fList ((Left unListData) d)) (\(u : unit) -> fI ((Left unIData) d)) (\(u : unit) -> fB ((Left unBData) d)) ()) d {data} (\(i : integer) -> \(ds : list (data)) -> fConstr i ((/\(a :: *) -> \(f : a -> a) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (/\(a :: *) -> \(b : bool) -> \(x : unit -> a) -> \(y : unit -> a) -> (Left ifThenElse) {unit -> a} b x y ()) {r} ((Left nullList) {a} x) (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x))) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Right Cons) {a} (f x) (rec xs')))) {data} rec ds)) (\(es : list (pair data data)) -> fMap ((/\(a :: *) -> \(f : a -> a) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (/\(a :: *) -> \(b : bool) -> \(x : unit -> a) -> \(y : unit -> a) -> (Left ifThenElse) {unit -> a} b x y ()) {r} ((Left nullList) {a} x) (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x))) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Right Cons) {a} (f x) (rec xs')))) {pair data data} ((/\(a :: *) -> \(f : a -> a) -> \(p : pair a a) -> (Right Comma) {a} {a} (f ((Left fstPair) {a} {a} p)) (f ((Left sndPair) {a} {a} p))) {data} rec) es)) (\(ds : list (data)) -> fList ((/\(a :: *) -> \(f : a -> a) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (/\(a :: *) -> \(b : bool) -> \(x : unit -> a) -> \(y : unit -> a) -> (Left ifThenElse) {unit -> a} b x y ()) {r} ((Left nullList) {a} x) (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x))) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Right Cons) {a} (f x) (rec xs')))) {data} rec ds)) fI fB)
+\(fConstr : integer -> list data -> data) -> \(fMap : list (pair data data) -> data) -> \(fList : list data -> data) -> \(fI : integer -> data) -> \(fB : bytestring -> data) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {data} {data} (\(rec : data -> data) -> \(d : data) -> (\(d : data) -> /\(r :: *) -> \(fConstr : integer -> list (data) -> r) -> \(fMap : list (pair (data) (data)) -> r) -> \(fList : list (data) -> r) -> \(fI : integer -> r) -> \(fB : bytestring -> r) -> (Left chooseData) {unit -> r} d (\(u : unit) -> (/\(a :: *) -> /\(b :: *) -> /\(c :: *) -> \(f : a -> b -> c) -> \(p : pair a b) -> f ((Left fstPair) {a} {b} p) ((Left sndPair) {a} {b} p)) {integer} {list (data)} {r} fConstr ((Left unConstrData) d)) (\(u : unit) -> fMap ((Left unMapData) d)) (\(u : unit) -> fList ((Left unListData) d)) (\(u : unit) -> fI ((Left unIData) d)) (\(u : unit) -> fB ((Left unBData) d)) ()) d {data} (\(i : integer) -> \(ds : list (data)) -> fConstr i ((/\(a :: *) -> \(f : a -> a) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Right Cons) {a} (f x) (rec xs')))) {data} rec ds)) (\(es : list (pair data data)) -> fMap ((/\(a :: *) -> \(f : a -> a) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Right Cons) {a} (f x) (rec xs')))) {pair data data} ((/\(a :: *) -> \(f : a -> a) -> \(p : pair a a) -> (Right Comma) {a} {a} (f ((Left fstPair) {a} {a} p)) (f ((Left sndPair) {a} {a} p))) {data} rec) es)) (\(ds : list (data)) -> fList ((/\(a :: *) -> \(f : a -> a) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Right Cons) {a} (f x) (rec xs')))) {data} rec ds)) fI fB)

plutus-core/plutus-core/test/Pretty/Golden/Readable/Examples/List/omapList.plc.golden

@@ -1 +1 @@
-/\(a :: *) -> \(f : a -> a) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (/\(a :: *) -> \(b : bool) -> \(x : unit -> a) -> \(y : unit -> a) -> (Left ifThenElse) {unit -> a} b x y ()) {r} ((Left nullList) {a} x) (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x))) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Right Cons) {a} (f x) (rec xs')))
+/\(a :: *) -> \(f : a -> a) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Right Cons) {a} (f x) (rec xs')))

plutus-core/plutus-core/test/Pretty/Golden/Readable/StdLib/Data/List/CaseList.plc.golden

@@ -1 +1 @@
-/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (/\(a :: *) -> \(b : bool) -> \(x : unit -> a) -> \(y : unit -> a) -> ifThenElse {unit -> a} b x y ()) {r} (nullList {a} x) (\(u : unit) -> z) (\(u : unit) -> f (headList {a} x) (tailList {a} x))
+/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> chooseList {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f (headList {a} x) (tailList {a} x)) ()

plutus-core/plutus-core/test/Pretty/Golden/Readable/StdLib/Data/List/FoldList.plc.golden

@@ -0,0 +1 @@
+/\(a :: *) -> /\(r :: *) -> \(f : r -> a -> r) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {r} {list a -> r} (\(rec : r -> list a -> r) -> \(z : r) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> chooseList {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f (headList {a} x) (tailList {a} x)) ()) {a} xs {r} z (\(x : a) -> \(xs' : list a) -> rec (f z x) xs'))

plutus-core/plutus-core/test/Pretty/Golden/Readable/StdLib/Data/List/FoldrList.plc.golden

@@ -1 +1 @@
-/\(a :: *) -> /\(r :: *) -> \(f : a -> r -> r) -> \(z : r) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {r} (\(rec : list a -> r) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> (/\(a :: *) -> \(b : bool) -> \(x : unit -> a) -> \(y : unit -> a) -> ifThenElse {unit -> a} b x y ()) {r} (nullList {a} x) (\(u : unit) -> z) (\(u : unit) -> f (headList {a} x) (tailList {a} x))) {a} xs {r} z (\(x : a) -> \(xs' : list a) -> f x (rec xs')))
+/\(a :: *) -> /\(r :: *) -> \(f : a -> r -> r) -> \(z : r) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \(a :: *) -> self a -> a) (a -> b) (\(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> ifix (\(self :: * -> *) -> \(a :: *) -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {r} (\(rec : list a -> r) -> \(xs : list a) -> (/\(a :: *) -> \(x : list a) -> /\(r :: *) -> \(z : r) -> \(f : a -> list a -> r) -> chooseList {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f (headList {a} x) (tailList {a} x)) ()) {a} xs {r} z (\(x : a) -> \(xs' : list a) -> f x (rec xs')))