gistfile1.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}

module Achiral.Internal where
import Data.Singletons
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Constraint
import GHC.Prim
import qualified Data.Constraint as D
import Data.Vinyl

-- My plan is present a quotient type of Vinyl, where is has a set of types instead of a list. 
-- Some cribbed code from HList repurposed.

class HEq (x :: k) (y :: k) (b :: Bool) | x y -> b where

instance HEq x x True 
instance False ~ b => HEq x y b 

class Insert x (ys :: [k]) (rs :: [k]) | x ys -> rs where
    insert :: f x -> Rec f ys -> Rec f rs

instance Insert x '[] '[x] where
    insert x RNil = x :& RNil

instance (HEq x y b, Insert' b x (y ': ys) rs) => Insert x (y ': ys) rs where
    insert = insert' (Proxy :: Proxy b)

class Insert' (b :: Bool) x (ys :: [k]) (rs :: [k]) | b x ys -> rs where
    insert' :: Proxy b -> f x -> Rec f ys -> Rec f rs

instance Insert' False x '[] '[x] where
    insert' _ x RNil = x :& RNil

instance Insert x ys rs => Insert' False x (y ': ys) (y ': rs) where
    insert' _ x (y :& ys) = y :& insert x ys

-- TODO
-- do remove
-- do subset
-- do element of -- lens
--  make the product of "basis" lenses
-- do equals
-- do diff
-- do patch
-- you can map over the values
-- you can traverse
-- you can union
-- you can intersect