church.hs

{-# LANGUAGE RankNTypes #-}

newtype ListC a = ListC
    { foldC :: forall r. (a -> r -> r) -> r -> r
    }

foldC' :: (a -> r -> r) -> r -> ListC a -> r
foldC' co ni (ListC f) = f co ni

isNil :: ListC a -> Bool
isNil (ListC f) = f (\ _ _ -> False) True

nilC :: ListC a
nilC = ListC (\ _ ni -> ni)

consC :: a -> ListC a -> ListC a
consC x l@(ListC f) = ListC (\ co ni -> co x (f co ni))

uncons :: (a -> ListC a -> r) -> r -> ListC a -> r
uncons co ni (ListC f) =
    let (headC,tailC) =
            f
                (\x (headC,tailC) ->
                      case headC of
                          Nothing -> (Just x, tailC)
                          Just _ -> (headC, consC x tailC))
                (Nothing, nilC)
    in case headC of
           Just x -> co x tailC
           Nothing -> ni

toList = uncons (\x xs -> x : toList xs) []