Proxy型

前提としてread, showの型はこう

code:hs

read :: Read a => String -> a

show :: Show a => a -> String

これを組み合わせたような関数を定義すると、

code:hs

f = show . read

かと言って、こういうふうにも定義できない

code:hs

f :: (Read a, Show a) => String -> String

f = show . read

code:hs

g :: forall a. (Read a, Show a) => a -> String -> String

g _ = (show :: a -> String) . read

要は、こういうノリのことがしたい

code:hs

g Int "3"

でも、Haskellは依存型を扱うわけではないので、型を値として扱えない

こうやって利用できる

code:hs

g 0 "3"

型情報を伝えるのが責務なのであれば、よりそれに制限されていたほうが良い

そこで、Proxyを使う

今回は自前で定義する

わかりやすさのため、値コンストラクタの名前をずらしている

code:hs

data Proxy t = ProxyC

関数は高定義する

code:hs

f :: forall proxy a. (Read a, Show a) => proxy a -> String -> String

f _ = (show :: a -> String) . read

PureScriptでは

code:purs(hs)

class Read a where

read :: String -> a

f ::

∀ a.

Read a =>

Show a =>

Proxy a ->

String ->

String

f _ = (show :: a -> String) <<< read

こう使う

code:hs

f (ProxyC :: Proxy Int) "3"

これが、Proxyの存在意義の一つ

し、もっと簡潔に書ける

TypeApplicationsを使って簡潔に型アノテーションを書く

code:hs

main = do

print $ show @Int . read $ "42"

何が嬉しい？

Proxyの定義

無いとどうなる

同じ引数の者同士は同じもの？

Proxyという名前

tsで言うとどういうものになるのか

1つもGHC拡張使わずに嬉しい例を見てみたい

存在型のこと？

カッコつけて

わかりやさすたのため、こうする

code:hs

data Proxy t = ProxyC

code: (hs)

ghci> import Data.Proxy

ghci> :t ProxC

ProxyC :: Proxy t

ghci> :t ProxyC :: Proxy Int

ProxyC :: Proxy Int :: Proxy Int

わかると自明だが、

code:hs

data Proxy t = Proxy deriving Bounded

code:purs(hs)

data Proxy :: forall k. k -> Type

data Proxy a = Proxy

任意のkindの型を引数に取る

code:purs(hs)

data SProxy :: Symbol -> Type

data SProxy sym = SProxy

Symbolを引数に取る

本当は型レベルの計算において、モノとモノを区別するためにタグ付けするために使う感じ

ただ、実際には関数も必要になるので(?)、関数側には値コンストラクタを与えるてきな?

code:purs(hs)

zero :: Proxy Zero

zero = Proxy

終対象

Voidに型パラメータを与えたようなもの

データは何も持たない