Created
February 10, 2023 09:16
-
-
Save peterstorm/96449bbece9bbb42b44c27b3a241b81c to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE AllowAmbiguousTypes #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# 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 | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment