ToggleList.idr

module Data.ToggleList

%access public export
%default total

data Next = A | B

next : Next -> Type -> Type -> Type
next A a _ = a
next B _ b = b

after : Next -> Next
after A = B
after B = A

data ToggleList : Next -> Type -> Type -> Type where
  Nil : ToggleList B a b
  (::) : {n : Next} -> next n a b -> ToggleList n a b -> ToggleList (after n) a b

PairedList : Type -> Type -> Type
PairedList a b = ToggleList B a b

stringIntList : PairedList String Int
stringIntList = ["hello", 1, "world", 2]

toTupleList : PairedList a b -> List (a, b)
toTupleList [] = []
toTupleList ((::) {n=A} x ((::) {n=B} y xs)) = (x, y) :: toTupleList xs

fromTupleList : List (a, b) -> PairedList a b
fromTupleList [] = []
fromTupleList ((x, y) :: xs) = x :: y :: fromTupleList xs