Proxy型
>#WIP
https://stackoverflow.com/a/27047260 の前半の説明などを読んで
前提としてread, showの型はこう
hsread :: Read a => String -> a
show :: Show a => a -> Stringこれを組み合わせたような関数を定義すると、
hsf = show . readこれは普通に考えれば型は、
String -> String だが、そうすると Read a や Show a の制約が消えてしまうので型安全でないそのため
f :: String -> String のような型注釈はエラーになるかと言って、こういうふうにも定義できない
hsf :: (Read a, Show a) => String -> String
f = show . readこれは、
a に制約を入れているが、結局、引数にも戻り値にも a が現れていないため、エラーになる使用する側から見ても
f "hoge" のようになるので、これだけではどういう中間型 a を経過すればよいのかわかるはずもないそこで、
a を使用するために、例えばこういう定義ができるhs{-# LANGUAGE ScopedTypeVariables #-}
g :: forall a. (Read a, Show a) => a -> String -> String
g _ = (show :: a -> String) . readただただ
a を型情報を得るためだけに引数に取っている要は、こういうノリのことがしたい
hsg Int "3"でも、Haskellは依存型を扱うわけではないので、型を値として扱えない
こうやって利用できる
hsg 0 "3"この
0 は数値なら何でもよく、 1 でも 100 でも何でも良いただ単に
Int ですよ、というのが伝われば良いでも、こう書くと「
0 ってなに？？」となる型情報を伝えるのが責務なのであれば、よりそれに制限されていたほうが良い
そこで、Proxyを使う
今回は自前で定義する
わかりやすさのため、値コンストラクタの名前をずらしている
hsdata Proxy t = ProxyC関数は高定義する
hs{-# LANGUAGE ScopedTypeVariables #-}
f :: forall proxy a. (Read a, Show a) => proxy a -> String -> String
f _ = (show :: a -> String) . readPureScriptでは
purs(hs)class Read a where
read :: String -> a
f ::
∀ a.
Read a =>
Show a =>
Proxy a ->
String ->
String
f _ = (show :: a -> String) <<< readこう使う
hsf (ProxyC :: Proxy Int) "3"最終的には
Int であることが伝わればよいのだが、値である
ProxyC を見ただけでは、型の Proxy a の a が確定しないため、 :: で明示する必要がある結果的にかなり冗長になっているが、仕方がない
これが、Proxyの存在意義の一つ
他の例はまだよく知らん
これに関しては、これはTypeApplicationsを使えばProxyは不要になる
し、もっと簡潔に書ける
TypeApplicationsを使って簡潔に型アノテーションを書く
hs{-# LANGUAGE TypeApplications #-}
main = do
print $ map (read @Int) ["33", "4"]
print $ show @Int . read $ "42"何が嬉しい？
Proxyの定義
無いとどうなる
同じ引数の者同士は同じもの？
Proxyという名前
tsで言うとどういうものになるのか
1つもGHC拡張使わずに嬉しい例を見てみたい
TypeApplicationsがあれば不要だったりする？
存在型のこと？
カッコつけて
わかりやさすたのため、こうする
hsdata Proxy t = ProxyC (hs)ghci> import Data.Proxy
ghci> :t ProxC
ProxyC :: Proxy t
ghci> :t ProxyC :: Proxy Int
ProxyC :: Proxy Int :: Proxy Intわかると自明だが、
1つ目の方は、「ProxyCの型は？」と聞いて、
Proxy t です、と返ってきている2つ目は、「
ProxyC :: Proxy Int の型は？」と聞いて、 Proxy Int ですと返ってきている括弧を付けるなら、
((ProxyC) :: Proxy Int) :: Proxy Int のような感じ「
1 :: Int の型は？」と聞いて、「 Int です(そらそう)」と返ってきているのと同じhsdata Proxy t = Proxy deriving Boundedpurs(hs)data Proxy :: forall k. k -> Type
data Proxy a = Proxy任意のkindの型を引数に取る
purs(hs)data SProxy :: Symbol -> Type
data SProxy sym = SProxySymbolを引数に取る
Proxyでもあるので、この値は、
Proxy 型を要請する場でも適用できる本当は型レベルの計算において、モノとモノを区別するためにタグ付けするために使う感じ
ただ、実際には関数も必要になるので(?)、関数側には値コンストラクタを与えるてきな?
purs(hs)zero :: Proxy Zero
zero = Proxy Void と同じようなもの終対象
Voidに型パラメータを与えたようなもの
データは何も持たない
AllowAmbiguousTypesを使えばProxyは不要？
幽霊型を使ってType-Level Literalsをやる
tsのliteral typeみたいなやつ