todo: find solution for head list

pcp/pcp.hs

@@ -3,8 +3,9 @@
 module Pcp where
 
 type LCBool = forall a.a -> a -> a
+-- newtype LCBoolC = LCBoolC { unBool :: LCBool }
 
-ite :: forall a. LCBool -> a -> a -> a
+ite :: (t1 -> t2 -> t3) -> t1 -> t2 -> t3
 ite = \c a b -> c a b
 
 true :: LCBool
@@ -61,8 +62,8 @@ prepa = \s -> LCStr $ \x a b -> a (unChurch s x a b)
 prepb :: LCStr -> LCStr
 prepb = \s -> LCStr $ \x a b -> b (unChurch s x a b)
 
-type LCPairSam = (LCStr -> LCStr -> LCStr) -> LCStr
-newtype LCPair = LCPair { unPair :: LCPairSam }
+-- type LCPairSam = (LCStr -> LCStr -> LCStr) -> LCStr
+-- newtype LCPair = LCPair { unPair :: LCPairSam }
 
 pair :: a1 -> a2 -> (a1 -> a2 -> a) -> a
 pair = \a -> \b -> \c -> c a b
@@ -73,31 +74,6 @@ first = \p -> p (\x -> \y -> x)
 second :: ((a1 -> a2 -> a2) -> a) -> a
 second = \p -> p (\x -> \y -> y)
 
--- Church Pairs (nil)
--- pair true true
-nil :: ((a1 -> a1 -> a1) -> (a2 -> a2 -> a2) -> a) -> a
-nil = pair true true
-
--- Church Comparison (is_nil)
--- first (true for nil pair)
-is_nil :: ((a2 -> a1 -> a2) -> a) -> a
-is_nil = first
-
--- Church Cons
--- λh.λt.pair false (pair h t)
-cons :: a2 -> a3 -> ((a1 -> a1 -> a1) -> ((a2 -> a3 -> a4) -> a4) -> a) -> a
-cons = \h -> \t -> pair false (pair h t)
-
--- Church Head
--- λz.first (second z)
-head :: ((a3 -> a4 -> a4) -> (a2 -> a1 -> a2) -> a) -> a
-head = \z -> first (second z)
-
--- Church Tail
--- λz.second (second z)
-tail :: ((a3 -> a4 -> a4) -> (a1 -> a2 -> a2) -> a) -> a
-tail = \z -> second (second z)
-
 nexta :: ((a2 -> a1 -> a2) -> LCStr) -> (LCStr -> LCStr -> a) -> a
 nexta = \x -> pair (prepa (first x)) (first x)
 
@@ -132,7 +108,43 @@ eq = ycomb (\f x y ->
   (land (hd_eq x y) (f (tl x) (tl y))))
 
 prefix :: LCStr -> LCStr -> LCBool
-prefix = \a b -> ycomb (\f x y -> ite (isempty x) true (land (hd_eq x y) (f (tl x) (tl y)))) a b
+prefix = ycomb (\f x y -> ite (isempty x) true (land (hd_eq x y) (f (tl x) (tl y))))
+
+-- LISTS
+-- type LCListSam = forall a.(a -> a -> a) -> a -> a
+-- newtype LCList = LCList { unList :: LCListSam }
+
+-- type LCListSam a = forall b . (a -> b -> b) -> b -> b
+type LCListSam b = forall a . (b -> a -> a) -> a -> a
+newtype LCList b = LCList { unList :: LCListSam b }
+
+-- List (nil)
+nil :: LCList a
+nil = LCList $ \c -> \n -> n
+
+-- List Cons
+cons :: a -> LCList a -> LCList a
+-- cons = \h t -> LCList $ \c n -> c h (unList t c n)
+cons = \h t -> LCList $ \c n -> c h (unList t c n)
+
+is_nil :: LCList a -> LCBool
+-- is_nil = \x -> unList x (\h t -> false) true
+is_nil = \l -> unList l (\h t -> false) true
+
+-- -- List Head
+-- hd_l :: LCList a -> a
+-- hd_l = \x -> unList x true nil
+hd_l = \l -> l (\h t -> h) nil
+-- hd_l = \l -> unList l (\h t -> h) nil
+
+-- List Tail
+next_l = \h p -> pair (cons h (first p)) (first p)
+
+tl_l :: LCList a -> LCList a
+tl_l = \l -> second (unList l next_l (pair nil nil))
+
+lent = ycomb (\f x -> ite (is_nil x) 0 (1 + (f (tl_l x))))
+-- flat = ycomb (\f x -> ite (is_nil x) "" ((hd_l x) ++ (f (tl_l x))))
 
 lcstr_tostr :: LCStr -> String
 lcstr_tostr = \s -> unChurch s ("") (\a -> "a" ++ a) (\b -> "b" ++ b)

pcp/test.hs

+type LCBool a = a -> a -> a
+
+true :: a -> a -> a
+true = \x y -> x
+
+false :: a -> a -> a
+false = \x y -> y
+
+type LCListSam a = (a -> a -> a) -> a -> a
+newtype LCList a = LCList { unList :: LCListSam a }
+
+-- List (nil)
+nil :: (a -> a -> a)
+nil = \c n -> n
+-- nil = \x -> true
+
+is_nil :: LCList (b -> b -> b) -> (b -> b -> b)
+is_nil = \x -> unList x (\h t -> false) true
+-- is_nil = \l -> l (\h t -> false)
+
+-- List Cons
+-- -- cons = \h t -> LCList $ \c n -> c h (unList t c n)
+cons :: a -> LCList a -> LCList a
+cons = \h t -> LCList $ \c n -> c h (unList t c n)
+
+-- List Cons
+-- List Head
+hd_l :: LCList (a -> a -> a) -> (a -> a -> a)
+-- hd_l = \x -> unList x true nil
+hd_l = \x -> unList x true nil
+
+next_l = \h p -> pair (cons h (first p)) (first p)
+
+-- tl_l :: LCList a -> LCList b
+tl_l = \l -> second (l next_l (pair nil nil))