関係と代数的データ型との相互変換についての妄想 その2

Haskell

思い付き その1

型レベルのリストをクエリー函数に与えてやる。（DataKinds が有効）

data Attr = Id | Name | Friends
data User = User { id :: Int, name :: String, friends :: [User] }
query :: Proxy '[??] -> Key -> MonadDB User
userFriends :: Proxy '[Friends] -> User -> [User]

リストだとダメだなーって気付いた。勝手に型の和が取られるわけじゃないからね。

それはそれとして、分からないところが2点。

1つは上記のコードで query の型の ?? って書いているところをどう書けばよいか。やりたいことは「?? の部分に入るのは 'Attr カインドの任意の型」ということを示したい。

しばらく寝かせて思い付いたけど KindSignatures を有効にして下記でいけるっぽい。

data ProxyAttr (t :: [Attr]) = ProxyAttr

もう1つは、下記のをうまいこと推論してくれないのなんでだ。stack --resolver lts-8.12 exec -- ghci -fprint-explicit-kinds -XDataKinds にて。

後から気付いた ProxyAttr を使うとエラーにならなかった。

ghci> :m + Data.Proxy
ghci> data Attr = Id | Name | Friends
ghci> data User = User { id :: Int, name :: String, friends :: [User] } deriving (Show)
ghci> :{
ghci| userFriends :: Proxy '[Friends] -> User -> [User]
ghci| userFriends _ _ = [User 1 "Ada" []]
ghci| :}
ghci> bob = User 2 "Bob" []
ghci> let p = Proxy in userFriends p bob

<interactive>:9:30: error:
    • Couldn't match type ‘*’ with ‘[Attr]’
      Expected type: Proxy [Attr] ((':) Attr 'Friends ('[] Attr))
        Actual type: Proxy * ((':) Attr 'Friends ('[] Attr))
    • In the first argument of ‘userFriends’, namely ‘p’
      In the expression: userFriends p bob
      In the expression: let p = Proxy in userFriends p bob

Proxy に型注釈してやると大丈夫。

ghci> let p = Proxy :: Proxy '[Friends] in userFriends p bob
[User {id = 1, name = "Ada", friends = []}]

どっちにしろリストの戦略は破綻してるのでボツ。

制約の方に情報を乗せないとあかん気がしている。