{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances   #-}
module Zinza.Indexing where

import Data.Functor.Identity (Identity (..))

class Indexing v i | i -> v, v -> i where
    extract :: i a -> a
    index   :: v a -> i b -> (a, b)

instance Indexing Identity Identity where
    extract :: forall a. Identity a -> a
extract = Identity a -> a
forall a. Identity a -> a
runIdentity
    index :: forall a b. Identity a -> Identity b -> (a, b)
index (Identity a
a) (Identity b
b) = (a
a, b
b)

data Idx f a
    = Here a
    | There (f a)

data Cons f a = a ::: f a

instance Indexing v i => Indexing (Cons v) (Idx i) where
    extract :: forall a. Idx i a -> a
extract (Here a
b)   = a
b
    extract (There i a
bs) = i a -> a
forall a. i a -> a
forall (v :: * -> *) (i :: * -> *) a. Indexing v i => i a -> a
extract i a
bs

    index :: forall a b. Cons v a -> Idx i b -> (a, b)
index (a
a ::: v a
_)  (Here b
b)   = (a
a, b
b)
    index (a
_ ::: v a
as) (There i b
bs) = v a -> i b -> (a, b)
forall a b. v a -> i b -> (a, b)
forall (v :: * -> *) (i :: * -> *) a b.
Indexing v i =>
v a -> i b -> (a, b)
index v a
as i b
bs