{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeSynonymInstances  #-}

module List where

import Base

-- Standard list type, interesting because of the
-- type parameter.

data List :: * -> * -> * where
  List :: List a [a]

type instance PF (List a) = K () :+: (K a :*: Id [a])

instance Ix (List a) [a] where
  ix = List
  from []     = L (K ())  
  from (x:xs) = R (K x :*: Id (I xs))
  to (L (K ())) = []
  to (R (K x :*: Id (I xs))) = x : xs