TypeDict.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.TypeDict (
  TypeDict (..),
  Get (..),
  (:::) (..),
  Key (..),
) where

import GHC.Records (HasField (getField))
import GHC.TypeLits (ErrorMessage (Text), KnownSymbol, Symbol, TypeError)

data TypeDict (keys :: [Type]) where
  Nil :: TypeDict '[]
  (::>) ::
    (KnownSymbol key) =>
    key ::: v ->
    TypeDict xs ->
    TypeDict (key ::: v ': xs)

infixr 5 ::>

data (key :: Symbol) ::: (value :: Type) :: Type where
  (:::) :: Key a -> v -> a ::: v
infixr 6 :::

data Key (k :: Symbol) = Key

instance l ~ l' => IsLabel (l :: Symbol) (Key l') where
  fromLabel = Key

data MembershipProof (key :: Symbol) (v :: Type) (keys :: [Type]) where
  Here :: MembershipProof key v ((key ::: v) : keys)
  There :: MembershipProof key v keys -> MembershipProof key v (t : keys)

type family
  MemberH
    (key :: Symbol)
    (keys :: [Type]) ::
    MembershipProof k v keys
  where
  MemberH key (key ::: v : keys) = 'Here
  MemberH key (_ ::: _ : keys) = 'There (MemberH key keys)
  MemberH key '[] =
    TypeError ('Text "The key is not present in this dict")

class Get (proof :: MembershipProof k v keys) | k keys -> v where
  getProof :: TypeDict keys -> v

instance Get 'Here where
  getProof (_ ::: x ::> _) = x

instance (Get l) => Get ('There l) where
  getProof (_ ::> xs) = getProof @_ @_ @_ @l xs

type Member k keys = (MemberH k keys :: MembershipProof k v keys)

instance
  (Get (Member k keys :: MembershipProof k v keys)) =>
  HasField k (TypeDict keys) v
  where
  getField = getProof @_ @_ @_ @(Member k keys)

{-
-- the '#v2' needs -XOverloadedLabels
dict :: TypeDict '["v1" ::: String, "v2" ::: Integer]
dict = Key @"v1" ::: "hello" ::> #v2 ::: 1 ::> Nil

getValue :: String
getValue = getField @"v1" dict
-}