是否可以刪除此DataKinds支持的異構列表實現的OverlappingInstances？

Question

隨着近期發佈的關於HaskellDB的文章，我一直有動力再次研究HList。因爲我們現在在GHC中有-XDataKinds，它實際上有一個異類列表的例子，所以我想調查HList如何使用DataKinds。到目前爲止，我有以下幾點：

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

可正常工作，但我在這個項目的目標是嘗試做無類型類儘可能。所以這裏有兩個問題。首先，是否有可能編寫(=?)（記錄字段存取器函數）而沒有類型類？如果不是，它可以寫在沒有重疊的情況下嗎？

我想我的第一個問題是不可能的，但也許第二個問題是可能的。我很想聽聽人們的想法！

Answer 1

我認爲這兩個問題的答案都是合格的否。你簡直不能有一個類型函數的形式

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

這實際上是什麼OverlappingInstances給你。 Oleg提出了一種使用TypeReps的替代機制，但我們還沒有。這個答案是合格的，因爲你必須醜陋「解決方案」，喜歡用分型

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

這顯然不是因爲類型類基於版本的一樣好。但是，如果你有一點點動態輸入...