module Lis  
where

infixr `cons'`
infixr `cons''`
infixr `cons'''`

-- basic implementation:

forlist      fnil fcons ls  = ls fnil fcons
cons    x xs fnil fcons     = fcons x xs
nil          fnil fcons     = fnil


{- "most general type" version: 
-}
forlist' = forlist
cons'    = cons
nil'     = nil

-- passes:
tail'      = forlist' undefined (\x xs -> xs)

-- doesn't pass:
-- map' f     = forlist' nil' (\x xs -> f x `cons'` map' f xs)


{- typed version with two type variables: 
   the first being the list element type,
   the second being the result type of the function that is 
   constructed with forlist.
   Enforces ls and (tail ls) to have the same type:
-}
newtype List'' a b = L'' (b -> (a -> List'' a b -> b) -> b) 

forlist'' fnil fcons (L'' ls) = forlist fnil fcons ls
nil''                         = L'' nil
cons'' x xs                   = L'' $ cons x xs

-- passes:
map'' f  = forlist'' nil'' (\x xs -> f x `cons''` map'' f xs) 

-- doesn't pass:
-- tail'' = forlist'' undefined (\x xs -> xs)

-- passes at the cost of copying the whole result:
repaired_tail'' = forlist'' undefined (\x xs -> map'' id xs)
		

{- typed version with three type variables: 
   the first being list element type,
   the second being the result type of the function which is constructed with forlist,
   the third being the result type of the function which consumes the list.
   Enforces (tail ls) and (tail (tail ls)) to have the same type:
-}
newtype List''' a b c = L''' (b -> (a -> List''' a c c -> b) -> b) 

forlist''' fnil fcons (L''' ls) = forlist fnil fcons ls
nil'''                       = L''' nil
cons''' x xs                 = L''' $ cons x xs

-- passes again:
map''' f  = forlist''' nil''' (\x xs -> f x `cons'''` map''' f xs) 

-- now passes:
tail''' = forlist''' undefined (\x xs -> xs)

-- doesn't pass:
-- tailtail''' ls = tail''' (tail''' ls)