È possibile rimuovere OverlappingInstances per questa implementazione di liste eterogenee con backup di DataKinds?

Question

Con i post recenti su HaskellDB, sono stato motivato a cercare di nuovo in HList. Dato che ora abbiamo -XDataKinds in GHC, che in realtà ha un esempio di liste eterogenee, ho voluto indagare su come HLists guardi con DataKinds. Finora, ho il seguente:

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

Questo funziona come previsto, ma il mio obiettivo in questo progetto è stato quello di cercare di farlo senza classi di tipo, per quanto possibile. Quindi ci sono 2 domande qui. In primo luogo, è possibile scrivere (=?) (la funzione accessor del campo record) senza una classe di tipo? In caso contrario, può essere scritto senza istanze sovrapposte?

Immagino che non sia possibile per la mia prima domanda, ma forse la seconda potrebbe essere possibile. Mi piacerebbe sentire cosa pensa la gente!

Answer 1

Penso che la risposta ad entrambe le domande sia una qualificata no. Semplicemente non puoi avere una funzione tipo del modulo

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

che è essenzialmente ciò che OverlappingInstances ti dà. Oleg ha suggerito un meccanismo alternativo usando TypeReps di livello di tipo, ma non ce l'abbiamo ancora. Questa risposta è qualificato, perché si ha brutti "soluzioni" come l'utilizzo di tipizzabile

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

questo non è chiaramente buono come la versione basata typeclass. Ma, se stai bene con un po 'di digitazione dinamica ...