TypeMap.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall #-}
module TypeMap where

import Data.SOP.NP
import Data.SOP.Constraint
import GHC.TypeLits
import Data.Kind
import Data.Proxy

-- $setup
-- >>> :set -XDataKinds

-- | Syntactically nicer pair, with 'Symbol' as first argument.
data KV = Symbol := Type

type family TheK (kv :: KV) :: Symbol where
    TheK (k := v) = k

type family TheV (kv :: KV) :: Type where
    TheV (k := v) = v

type k := v = k ':= v

-------------------------------------------------------------------------------
-- Sorted "singleton"
-------------------------------------------------------------------------------

data SortedProof :: [KV] -> Type where
    SortedNil :: SortedProof '[]
    SortedNE  :: SortedProofNE (k := v ': kvs) -> SortedProof (k := v ': kvs)

data SortedProofNE :: [KV] -> Type where
    SortedSing :: SortedProofNE '[k := v]
    SortedCons :: CmpSymbol k k' ~ 'LT => SortedProofNE (k' := v' : kvs) -> SortedProofNE (k := v : k' := v' : kvs)

-------------------------------------------------------------------------------
-- SortedProof can be computed by constaint solver
-------------------------------------------------------------------------------

class Sorted (kvs :: [KV]) where
    sortedProof :: SortedProof kvs

instance Sorted '[] where
    sortedProof = SortedNil

instance (SortedNE k v kvs, kv ~ (k := v)) => Sorted (kv ': kvs) where
    sortedProof = SortedNE sortedProofNE

class SortedNE (k :: Symbol) (v :: Type) (kvs :: [KV]) where
    sortedProofNE :: SortedProofNE (k := v : kvs)

instance SortedNE k v '[] where
    sortedProofNE = SortedSing

instance (CmpSymbol k k' ~ 'LT, SortedNE k' v' kvs, kv' ~ (k' := v')) => SortedNE k v (kv' : kvs) where
    sortedProofNE = SortedCons sortedProofNE

type Example = '[ "abc" := String, "def" := Bool ]

example01 :: SortedProof Example
example01 = sortedProof

-------------------------------------------------------------------------------
-- Heteregenous Symbol -> Map
-------------------------------------------------------------------------------

data Entry :: KV -> Type where
    Entry :: KnownSymbol k => v -> Entry (k := v)

instance Show v => Show (Entry (k := v)) where
    showsPrec d (Entry v)
        = showParen (d > 10)
        $ showString "Entry @"
        . shows (symbolVal (Proxy :: Proxy k))
        . showChar ' '
        . shows v

data TMap kvs where
    TMap :: Sorted kvs => NP Entry kvs -> TMap kvs

-- | >>> example02
-- TMap (Entry @"abc" "foo" :* Entry @"def" True :* Nil)
example02 :: TMap Example
example02 = TMap (Entry "foo" :* Entry True :* Nil)

-------------------------------------------------------------------------------
-- Show
-------------------------------------------------------------------------------

type family AllV (c :: Type -> Constraint) (kvs :: [KV]) :: Constraint where
    AllV c '[]         = ()
    AllV c (kv ': kvs) = (c (TheV kv), AllV c kvs)

deriving instance (All (Compose Show Entry) kvs) => Show (TMap kvs)

-------------------------------------------------------------------------------
-- Insert
-------------------------------------------------------------------------------

class (KnownSymbol k, Sorted kvs, Sorted (Inserted k v kvs)) => Insert (k :: Symbol) (v :: Type) (kvs :: [KV]) where
    type Inserted (k :: Symbol) (v :: Type) (kvs :: [KV]) :: [KV]
    
    insert :: Proxy k -> v -> TMap kvs -> TMap (Inserted k v kvs)

instance KnownSymbol k => Insert k v '[] where
    type Inserted k v '[] = '[k := v]

    insert _ v _ = TMap (Entry v :* Nil)

instance
    ( InsertNE (CmpSymbol k (TheK kv)) k v (TheK kv) (TheV kv) kvs
    , kv ~ (TheK kv := TheV kv)
    , KnownSymbol k
    , SortedNE (TheK kv) (TheV kv) kvs
    )
  =>
    Insert k v (kv ': kvs)
  where
    type Inserted k v (kv : kvs) = InsertedNE (CmpSymbol k (TheK kv)) k v (TheK kv) (TheV kv) kvs

    insert = insertNE (Proxy :: Proxy (CmpSymbol k (TheK kv)))

class (KnownSymbol k, o ~ CmpSymbol k k', SortedNE k' v' kvs, Sorted (InsertedNE o k v k' v' kvs)) => InsertNE (o :: Ordering) (k :: Symbol) (v :: Type) (k' :: Symbol) (v' :: Type) (kvs :: [KV]) where
    type InsertedNE o k v k' v' kvs :: [KV]

    insertNE :: Proxy o -> Proxy k -> v -> TMap (k' := v' : kvs) -> TMap (InsertedNE o k v k' v' kvs)

instance (KnownSymbol k, 'LT ~ CmpSymbol k k', SortedNE k' v' kvs) => InsertNE 'LT k v k' v' kvs where
    type InsertedNE 'LT k v k' v' kvs = (k := v : k' := v' : kvs)

    insertNE _ _ v (TMap m) = TMap (Entry v :* m)

instance (KnownSymbol k, 'GT ~ CmpSymbol k k', Insert k v kvs, SortedNE k' v' kvs, SortedNE k' v' (Inserted k v kvs)) => InsertNE 'GT k v k' v' kvs where
    type InsertedNE 'GT k v k' v' kvs = (k' := v' : Inserted k v kvs)

    insertNE _ proxy v (TMap (kv :* kvs)) =
        case insert proxy v (TMap kvs) of
            TMap    kvs' -> TMap (kv :* kvs')

-- | >>> example03
-- TMap (Entry @"abc" "foo" :* Entry @"def" True :* Entry @"xyz" 42 :* Nil)
--
-- >>> insert (Proxy :: Proxy "b") 'x' example03
-- TMap (Entry @"abc" "foo" :* Entry @"b" 'x' :* Entry @"def" True :* Entry @"xyz" 42 :* Nil)
example03 :: TMap (Inserted "xyz" Int Example)
example03 = insert (Proxy :: Proxy "xyz") (42 :: Int) example02