이 DataKinds를 지원하는 이기종 목록 구현을 위해 OverlappingInstances를 제거 할 수 있습니까?

Question

HaskellDB에 관한 최근 글이 있으면 HList를 다시 살펴볼 동기가 있습니다. GHC에 -XDataKinds이 있는데 실제로 이질적인 목록의 예가 있으므로 HL 키가 DataKind로 어떻게 보이는지 조사하고 싶습니다. 이것은 예상하지만,이 프로젝트의 내 목표 시도하고 가능한 한 많은 종류의 클래스없이 그것을 할 수 있었다으로 작동

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

: 지금까지, 나는 다음 있습니다. 여기에는 2 가지 질문이 있습니다. 첫째, 형식 클래스없이 (=?) (레코드 필드 접근 자 함수)을 쓸 수 있습니까? 그렇지 않다면 중복 인스턴스없이 작성할 수 있습니까?

내 첫 번째 질문에는 불가능하다고 생각하지만 두 번째 질문이 가능할 수도 있습니다. 나는 사람들이 생각하는 것을 듣고 싶다!

Answer 1

두 질문에 대한 대답은 아니요입니다. 당신은 단순히 형식의 유형 기능을 가지고 있습니다

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

이것은 본질적으로 OverlappingInstances가 당신에게주는 것입니다. Oleg는 TypeReps를 사용하는 대체 메커니즘을 제안했으나 아직 가지고 있지 않습니다. 이 명확하게 typeclass 기반 버전만큼 좋지 않아 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 

를 사용하여 같은 추악한 "솔루션"이 때문에이 대답은 자격이있다. 그러나 조금 동적 인 타이핑을해도 괜찮다면 ...