as_capabl
Map.insert k v <$> buildMap (ks, vs)
これはbuildMapが全部返ってきてからMaybeでパターンマッチする形になるから、確かにスタック積み上がりそう。こういう所はHaskellでも末尾再帰気にしないといけないんですね
Map.insert k v <$> buildMap (ks, vs)
data Hoge = II
huga x = x
main = do
i <- huga II
putStrLn "hello, world"
• Couldn't match expected type 'IO a0' with actual type 'Hoge'
• In a stmt of a 'do' block: i <- huga II
In the expression:
do i <- huga II
putStrLn "hello, world"
In an equation for 'main':
main
= do i <- huga II
putStrLn "hello, world"
|
5 | i <- huga II
| ^^^^^^^
data Hoge = II
huga x = x
main = do
i <- return II
putStrLn "hello, world"
data Hoge = II
huga x = x
main = do
i <- return II
putStrLn "hello, world"
return の型は Monad m => a -> m a であり、引数の型 (ここでは a という型変数で表されています) が Monad のインスタンスかどうかを気にしないからです…というのではどうでしょう?do記法でi <- e
eはなんらかの式）と書くと、 eは IO a型、 iは a型に推論されます。一つ目のプログラムではhuga IIは Hoge型であり、`IO a`型とマッチできないので型エラーが発生しています。return IIは Monad m => m Hogeという型に推論されます。これを IO a型とマッチさせると、 m = IO, a = Hogeという解が見つかるのでエラーは発生しません。
data Fool where
Fool :: ('True ~ 'False) => Fool
theFool :: Fool
theFool = ???
main :: IO ()
main = case theFool of
Fool -> pure ()
Fool 型の値は得られない(Emptyである)ことが証明できるので，得られません．
theFool :: Fool
theFool = case refl of {} where
refl :: (a ~ b) => a :~: b
refl = Refl
theFool = theFool も要件を満たしますがそういうことではないですよね。theFool = unsafeCoerce $ \_ -> () とか。unsafeCoerce () でも動くと思いますが Fool のarityは1になると思うので const () の方が良いかもしれません。｀Fool｀ 型の値は得られない(Emptyである)ことが証明できるので，得られません．
True ~ Falseほど邪悪なのではなくて、 SomeConstraint :: * -> Constraint をtype familyとして、data Cert a where Cert :: SomeConstraint a => Cert a
aがコンパイル時に分かっている場合には SomeConstraint aが簡約できてうまくいくんですが、 aが実行時にしかわからないケースもサポートしたくて、動的に SomeConstraint相当のチェックをしてから Certの値を作りたいという状況です。引数は使われないので ｀unsafeCoerce ()｀ でも動くと思いますが ｀Fool｀ のarityは1になると思うので ｀const ()｀ の方が良いかもしれません。やはり
unsafeCoerceを使うのが無難そうですね。data Cert a where ... ではなく data Cert where にして、あとはtheFoolにあたる関数theCertの型を theCert :: SomeConstraint a => a -> Cert とするイメージかなと思いますi <- e とかくとeはIO aに推論されるのでしょう？mainがIOのため？m = IO となります．Haskell では，do i <- e …
e >>= \i -> ...
>>= は https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:-62--62--61- の型を持つ型クラスのメソッドになります．今回は putStrLn "Hello World!" :: IO () が続くのでここから(>>=) :: m a -> (a -> m b) -> m b の m b の部分が IO () と一致すると判定され m = IO / b = () となりますm = IO から return II :: m Hoge の部分の m も m = IO と推論されますIO a0 の a0 は例えばf :: Maybe a -> () f _ = () g :: Maybe a -> () g _ = () h = f (g ())
f の引数における型変数 a のことなのか， g の引数における型変数 a のことなのか分からなくなることを避けるため，番号を暗黙に振り分けるということが内部で行われている結果です．確かに，少し分かりにくいですね．(>>=) :: m a -> (a -> m b) -> m bは ma と (a -> mb)の二つ引数をとるのに、`e = \i -> ...` だとe一つしか引数に取らないように見えますがどうなんでしょう？
data Hoge = II deriving (Show)
huga x = x
main = do
i <- return 3
let x = huga i
print $ 1
<- を >>= とラムダ式に、 let は let ... in ... に、逐次処理は >> でつなげばよい感じです。
data Hoge = II deriving (Show)
huga x = x
main =
return 3 >>= (\i -> let x = huga in return 1 ) >> print $ 1
do v <- e1 e2 ==> e1 >>= \v -> e2
do e1 e2 ==> do _ <- e1 e2
do
let v1 = e1
...
vN = eN
e
==>
let v1 = e1
...
vN = eN
in e
do e ==> e
do
line1
line2
…
lineN
==>
do
line1
do
line2
...
lineN
>> を使った変換)が行われたり， p <- e の p の部分にパターンが使われると fail という関数を使った変換が行われたりするのですが，厳密さを求めないなら大体は上の変換を想定してもらえば大丈夫だと思います)
do
i <- return 3
let x = huga i
print $ 1
==>
do
i <- return 3
do
let x = huga i
print $ 1
==>
return 3 >>= \i -> do
let x = huga i
print $ 1
==>
return 3 >>= \i ->
let x = huga i
in print $ 1
>>= で書き直せる感じですね)main = print 1