7

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

これは期待どおりに機能しますが、このプロジェクトでの私の目標は、可能な限り型クラスなしでそれを実行することでした。したがって、ここには2つの質問があります。(=?)まず、型クラスなしで（レコードフィールドアクセサ関数）を書くことは可能ですか？そうでない場合は、インスタンスを重複させずに書き込むことができますか？

私の最初の質問では不可能だと思いますが、2番目の質問は可能かもしれません。人々の意見を聞きたいです！

4

1 に答える 1

2

私は両方の質問への答えは修飾されたいいえだと思います。あなたは単にフォームの型関数を持つことができません

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

これは明らかに型クラスベースのバージョンほど良くありません。しかし、少し動的型付けで大丈夫なら...

于 2012-08-26T09:43:34.083 に答える