Is it possible to remove OverlappingInstances for this DataKinds-backed heterogeneous list implementation?

Question

With recent posts about HaskellDB, I've been motivated to look into HList again. As we now have -XDataKinds in GHC, which actually has an example of heterogeneous lists, I wanted to investigate how HLists look with DataKinds. So far, I have the following:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Tagged

data Record :: [*] -> * where
  RNil :: Record '[]
  (:*:) :: Tagged f (FieldV f) -> Record t -> Record (f ': t)

type family FieldV a :: *

emptyRecord = RNil

(=:) :: (v ~ FieldV f) => f -> v -> Tagged f v
f =: v = Tagged v

class HasField x xs where
  (=?) :: Record xs -> x -> FieldV x

instance HasField x (x ': xs) where
  (Tagged v :*: _) =? _ = v

instance HasField x xs => HasField x (a ': xs) where
  (_ :*: r) =? f = r =? f

--------------------------------------------------------------------------------
data EmployeeName = EmployeeName
type instance FieldV EmployeeName = String

data EmployeeID = EmployeeID
type instance FieldV EmployeeID = Int

employee =   (EmployeeName =: "James")
         :*: ((EmployeeID =: 5) :*: RNil)

employeeName = employee =? EmployeeName
employeeId   = employee =? EmployeeID

This works as expected, but my goal in this project was to try and do it without type classes as much as possible. So there are 2 questions here. Firstly, is it possible to write (=?) (the record field accessor function) without a type class? If not, can it be written without overlapping instances?

I imagine that it's not possible for my first question, but maybe the second may be possible. I'd love to hear what people think!

Joleen

Since the original HList paper managed to get away with only using MultiParamTypeClasses and FunctionalDependencies, I'd imagine just adding in (and using) DataKinds wouldn't change that. – Endocardial

@Ptharien'sFlame the HList paper uses overlappingInstances to implement TypeEq. Everything else can be done using TypeEq – Atlantes

@PhilipJF Then all you need is TypeFamilies and MultiParamTypeClasses, no TypeEq required! – Endocardial

Answer 1

I think the answer to both questions is a qualified no. You simply cant have a type function of the form

type family TypeEq a b :: Bool
type instance TypeEq a a = True
type instance TypeEq a b = False

which is essentially what OverlappingInstances gives you. Oleg has suggested an alternative mechanism using type level TypeReps, but we don't have it yet. This answer is qualified, because you do have ugly "solutions" like using typeable

{-# LANGUAGE DataKinds, GADTs, DeriveDataTypeable, TypeFamilies, TypeOperators #-}

import Data.Typeable

type family FieldV a :: *

data FieldOf f where
  FieldOf :: FieldV f -> FieldOf f

(=:) :: f -> FieldV f -> FieldOf f
_ =: v = FieldOf v

fromField :: FieldOf f -> FieldV f
fromField (FieldOf v) = v

data Record :: [*] -> * where
  RNil :: Record '[]
  (:*:) :: Typeable f => FieldOf f -> Record t -> Record (f ': t)

data SameType a b where
  Refl :: SameType a a

useProof :: SameType a b -> a -> b
useProof Refl a = a 

newtype SF a b = SF (SameType (FieldOf a) (FieldOf b))
sf1 :: FieldOf f -> SF f f
sf1 _ = SF Refl

targetType :: f -> Maybe (SF g f)
targetType _ = Nothing

(?=) :: Typeable a => Record xs -> a -> Maybe (FieldV a)
RNil ?= _ = Nothing
(x :*: xs) ?= a = case (gcast (sf1 x)) `asTypeOf` (targetType a) of
                   Nothing      -> xs ?= a
                   Just (SF y)  -> Just . fromField $ useProof y x

x =? v = case x ?= v of
          Just x -> x
          Nothing -> error "this implementation under uses the type system"

data EmployeeName = EmployeeName deriving Typeable
type instance FieldV EmployeeName = String

data EmployeeID = EmployeeID deriving Typeable
type instance FieldV EmployeeID = Int

employee =   (EmployeeName =: "James")
         :*: ((EmployeeID =: 5) :*: RNil)

employeeName = employee =? EmployeeName
employeeId   = employee =? EmployeeID

this is clearly not as good as the typeclass based version. But, if you are okay with a little dynamic typing...

Atlantes

Thanks, I'll take that as an answer! Out of all the options I'm not sure what I like best. We either get no data kinds, overlapping instances, or we have to bring Typeable in... – Joleen