¿Es posible eliminar OverlappingInstances para esta implementación de lista heterogénea respaldada por DataKinds?

Question

Con publicaciones recientes sobre HaskellDB, me he sentido motivado a buscar en HList nuevamente. Como ahora tenemos -XDataKinds en GHC, que en realidad tiene un ejemplo de listas heterogéneas, quería investigar cómo se ven los HLists con DataKinds. Hasta el momento, tengo el siguiente:

{-# 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 

Esto funciona como se esperaba, pero mi objetivo en este proyecto fue tratar de hacerlo sin clases de tipos tanto como sea posible. Entonces hay 2 preguntas aquí. En primer lugar, ¿es posible escribir (=?) (la función de acceso al campo de registro) sin una clase de tipo? Si no, ¿puede escribirse sin superponer instancias?

Imagino que no es posible para mi primera pregunta, pero quizás la segunda sea posible. Me encantaría escuchar lo que la gente piensa

Answer 1

Creo que la respuesta a ambas preguntas es un calificado no. Simplemente no puede tener una función de tipo del formulario

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

que es esencialmente lo que le brinda OverlappingInstances. Oleg ha sugerido un mecanismo alternativo utilizando TypeReps de tipo, pero todavía no lo tenemos. Esta respuesta es cualificado, porque usted tiene feos "soluciones" como el uso de tipificable

{-# 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 

esto claramente no es tan buena como la versión basada en la clase de tipos. Pero, si está bien con un poco de tipado dinámico ...