型レベルハンバーガーについての報告

Posted on 2017/06/26
Tags: [Haskell]

これは私的な近況報告です

 ここ4日くらいは型レベルプログラミングの体験をしていました!
その成果物である、型レベルハンバーガーはHamburger.hs及びHamburger/TH.hsから成ります。

出力結果

SHamburger (Space Space Space Space)
SHamburger (Cheese Space Space Space)
SHamburger (Cheese Tomato Space Space)
SHamburger (Cheese Tomato Meet Space)
SHamburger (Cheese Tomato Meet Ushi)
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

module Hamberger where

import Hamburger.TH (defineInstances)

-- | A kind of the topping, and types.
data Topping = Space -- ^ Mean a space, it can be inserted some @Topping@
             | Cheese | Tomato | Meet | Ushi

-- |
-- A type level function
-- that maps @HamburgerT@ and @Topping@ to @HamburgerT@.
--
-- If @HamburgerC a b c d@ :: @HamburgerT@ of the domain has no space, or @Fail@ is specified to the domain,
-- return @Fail@ type.
type family AddTopping (h :: HamburgerT) (t :: Topping) :: HamburgerT where
  AddTopping (HamburgerC Space b c d) t = HamburgerC t b c d
  AddTopping (HamburgerC a Space c d) t = HamburgerC a t c d
  AddTopping (HamburgerC a b Space d) t = HamburgerC a b t d
  AddTopping (HamburgerC a b c Space) t = HamburgerC a b c t
  AddTopping _ _ = Fail

-- | A kind of the abstract hamburger
data HamburgerT = HamburgerC Topping Topping Topping Topping -- ^ A type constructor of the abstract hamburger
                | Fail -- ^ Mean a fail of a mapping of @AddTopping@


{- The dependent type -}

-- |
-- A concrete of the hamburger
-- (A type constructor for a type of @HamburgerT@ kind).
data SHamburger (h :: HamburgerT) where
  Concrete :: STopping -> STopping -> STopping -> STopping -> SHamburger (HamburgerC a b c d :: HamburgerT)

-- | A singleton type for @Topping@ kind.
data STopping = SSpace | SCheese | STomato | SMeet | SUshi
  deriving (Show)

-- | Represent the simply dependent type
class Singleton (h :: HamburgerT) where
  sing :: SHamburger h


-- Define any instances for 126 patterns !
defineInstances


type BasicHamburgerC = HamburgerC Space Space Space Space

type HamburgerC1 = AddTopping BasicHamburgerC Cheese -- these kind is @HamburgerT@
type HamburgerC2 = AddTopping HamburgerC1 Tomato
type HamburgerC3 = AddTopping HamburgerC2 Meet
type HamburgerC4 = AddTopping HamburgerC3 Ushi
type HamburgerC5 = AddTopping HamburgerC4 Ushi -- = Fail

x0 = sing :: SHamburger BasicHamburgerC
x1 = sing :: SHamburger HamburgerC1
x2 = sing :: SHamburger HamburgerC2
x3 = sing :: SHamburger HamburgerC3
x4 = sing :: SHamburger HamburgerC4
--x5 = sing :: SHamburger HamburgerC5 -- This is the compile error because Refl is not a Fail's value


main :: IO ()
main = do
  print x0
  print x1
  print x2
  print x3
  print x4
{-# LANGUAGE TemplateHaskell #-}

module Hamburger.TH where

import Language.Haskell.TH (Type(..), Name, mkName, Exp(..), DecsQ, Dec(..), Clause(..), Pat(..), Body(..), Lit(..))

type TypeName = String

type Topping4 = (TypeName, TypeName, TypeName, TypeName)


topping4s :: [Topping4]
topping4s = [(w, x, y, z) | w <- toppings, x <- toppings, y <- toppings, z <- toppings]
  where
    toppings :: [TypeName]
    toppings = ["Space", "Cheese", "Tomato", "Meet", "Ushi"]

-- | Make a AST of @Type@ is like "(HamburgerC Space Cheese Tomato Meet)"
hamburgerC :: Topping4 -> Type
hamburgerC (w, x, y, z) = ParensT (ConT (mkName "HamburgerC") 
                            `AppT` ConT (mkName w)
                            `AppT` ConT (mkName x)
                            `AppT` ConT (mkName y)
                            `AppT` ConT (mkName z))

-- |
-- Make a AST of @Exp@ is like "Concrete SSpace SCheese STomato SMeet"
-- (@Topping4@ elements are added "S" prefix for @STopping@).
concrete :: Topping4 -> Exp
concrete (w, x, y, z) = ConE (mkName "Concrete")
                 `AppE` ConE (mkName $ "S" ++ w)
                 `AppE` ConE (mkName $ "S" ++ x)
                 `AppE` ConE (mkName $ "S" ++ y)
                 `AppE` ConE (mkName $ "S" ++ z)


-- | Define @Singleton@ instances and @Show@ instances for any pattern of @topping4@
defineInstances :: DecsQ
defineInstances = do
  let singletonInstances = map defineSingletonInstance topping4s
      showInstances      = map defineShowInstance topping4s
  return $ singletonInstances ++ showInstances
  where
    defineSingletonInstance :: Topping4 -> Dec
    defineSingletonInstance t4@(w, x, y, z) =
      InstanceD Nothing []
        (ConT (mkName "Singleton") `AppT` hamburgerC t4)
        [
          FunD (mkName "sing") [Clause [] (NormalB $ concrete t4) []]
        ]

    defineShowInstance :: Topping4 -> Dec
    defineShowInstance t4@(w, x, y, z) =
      InstanceD Nothing []
        (ConT (mkName "Show") `AppT` ParensT (ConT (mkName "SHamburger") `AppT` hamburgerC t4))
        [
          FunD (mkName "show") [Clause [WildP] (NormalB $
              (LitE . StringL $ "SHamburger (" ++ w ++ " " ++ x ++ " " ++ y ++ " " ++ z ++ ")")
          ) []]
        ]

解説

型レベルハンバーガーの目的、主題

 型レベルハンバーガーは

  1. 5つ以上のトッピングを追加されると、例外ではなくコンパイルエラーで失敗を報告します
  2. 失敗していない有効なハンバーガーは、値として取得できます

というのが目的(主題)です。 (2つ目のやつは後付け)

詳細にはこんな感じ。

  1. 5つ以上のToppingを追加されると(x5を介して)コンパイルエラーになります
  2. Toppingの追加はTypeFamiliesの型関数AddToppingによって追加されます
  3. Toppingの追加は種HamburgerTの型Hamburger a b c dに対して行われます
    • type family AddTopping (h :: HamburgerT) (t :: Topping) :: HamburgerT
    • (擬似的にはHamburgerT -> Topping -> HamburgerT
  4. HamburgerTを持つ型のうち有効なもの(つまりFail以外)は値レベルに降格できます
    • 備考: 依存型って、値から型への昇格を扱うだけのものじゃなかったんだね

型レベルハンバーガーの見どころ

 これの見どころ(こだわりどころ)は、Hamburger.hsのトップレベルにあるx5をコンパイルしようとすると、コンパイルエラーになるところです。
それは、x5の型であるSHamburger HambergerC5SHamburger Failであり (※:kind!FailはHamburger.hsに定義されている型クラスSingletonのインスタンスではないからです。 (sing関数はSingletonの関数)

 以下の型のSingletonインスタンスは

TemplateHaskellによってHamburger.hsのトップレベルで展開されるdefineInstancesによって定義されます。 defineInstancesはTH.hsによって提供されているメタ関数です。

型レベルハンバーガーへのToppingの追加

type family AddTopping (h :: HamburgerT) (t :: Topping) :: HamburgerT where
  AddTopping (HamburgerC Space b c d) t = HamburgerC t b c d
  AddTopping (HamburgerC a Space c d) t = HamburgerC a t c d
  AddTopping (HamburgerC a b Space d) t = HamburgerC a b t d
  AddTopping (HamburgerC a b c Space) t = HamburgerC a b c t
  AddTopping _ _ = Fail

 このパターンそのまんまですね、TypeFamiliesです。

型レベルプログラミングを解決するためにTemplateHaskellを使うのは1回 回った感がある(TH.hsについて)

 TH.hsにあるdefineInstancesSHamburger (HamburgerC a b c d :: HamburgerT)の形をした126個の型のSingletonインスタンスを生成します。 (つまりSHamburger (h :: HamburgerT)のうちFail以外に対する)

 Singletonは依存型(もどき?)を扱うためのものです。

 参考にしたページでは自然数の帰納法を使ってインスタンスを実装してましたが、 依存型を使うことを考える前に考えた構造が全然帰納的でなかったので、TemplateHaskellを使って力技で解決しました。 (誰かうまい方法を教えてください!)

値レベルハンバーガー

data SHamburger (h :: HamburgerT) where
  Concrete :: STopping -> STopping -> STopping -> STopping -> SHamburger (HamburgerC a b c d :: HamburgerT)

data STopping = SSpace | SCheese | STomato | SMeet | SUshi
  deriving (Show)

 各Singletonインスタンス実装はdefineInstancesが行うので具体的なコードはありませんが、このようなものになります。

instance Singleton (HamburgerC Cheese Ushi Meet Space) where
  sing = Concrete SCheese SUshi SMeet SSpace

 Haskellでは依存型は実際には使えないらしいので、インスタンスになる型とsing(の具体値)はこのような一対一対応になります。

型レベル: HamburgerC Cheese Ushi Meet Space
値レベル: Concrete SCheese SUshi SMeet SSpace

HamburgerCCheese Ushi Meet Spaceが指定されれば、その値はConcreteSCheese SUshi SMeet SSpaceに限り
その逆もまた同じく限る感じです。

一意的ってことですね。

ということで

 進捗報告はこんな感じでした 🐕

元ネタ

@ U科各位

Java課題ソースコードhttps://t.co/NOUtZAxB44

— 焼きそばメロンパン@🍣 (@ice_arr) 2017年6月19日

参考

Special Thanks !



この記事はこちらから修正リクエストを送ることができます。
型レベルハンバーガーについての報告 - github
ゴミ箱ボタンの左にある、鉛筆ボタンを押してね!