haskell-jp / questions #104 at 2023-10-01 14:18:39 +0900

forallを用いたデータ型について質問です．
以下の通りに`AnyBar`型を構成した場合に，値を取り出す関数を書きたいです．

{-# LANGUAGE ExistentialQuantification #-}

module Bar where

data AnyBar b = forall a. AnyBar a (a -> b)

argBar :: AnyBar b -> b
argBar (AnyBar x f) = f x

letBar :: AnyBar b -> b
letBar ab = let AnyBar x f = ab in f x

2通りのうち`letBar`だけエラーになりました．

src/Bar.hs:11:26: error:
    • Couldn't match expected type 'p1' with actual type 'a -> b'
      'p1' is a rigid type variable bound by
        the inferred types of
          x :: p
          f :: p1
        at src/Bar.hs:11:17-31
    • In the pattern: AnyBar x f
      In a pattern binding: AnyBar x f = ab
      In the expression: let AnyBar x f = ab in f x
    • Relevant bindings include
        ab :: AnyBar b (bound at src/Bar.hs:11:8)
        letBar :: AnyBar b -> b (bound at src/Bar.hs:11:1)
   |
11 | letBar ab = let AnyBar x f = ab in f x
   |                          ^

原因が分からないです．見た感じだと両者ともパターンマッチしてるだけで差異が現れるとは思えません．

使用バージョンはghc-9.2.7です．

GHC User’s guide にそのものまんまの正気とは思えない記述がありました：

GHC User’s Guide (GHC 9.6.3), 6.4.6.3 Restrictions, in section 6.4.6 Existentially quantified data constructors
https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/existential_quantification.html#restrictions

> You can’t pattern-match on an existentially quantified constructor in a let or wheregroup of bindings. So this is illegal:
>

f3 x = a==b where { Baz1 a b = x }

> Instead, use a case expression:
>

f3 x = case x of Baz1 a b -> a==b

> In general, you can only pattern-match on an existentially-quantified constructor in a case expression or in the patterns of a function definition.

ありがとうございます．仕様と言われると引き下がるしかありませんね．

GADTs をオンにするともうちょっとどういう扱いでダメということになっているかがわかりやすいエラーが出ますね：

ghci> :set -XExistentialQuantification 
ghci> data T b = forall a. T a (a -> b)
ghci> :set -XGADTs
ghci> :{
ghci| f1 :: T b -> b
ghci| f1 t = let T a f = t in f a
ghci| :}

<interactive>:25:14: error:
    • Couldn't match expected type 't0' with actual type 'a'
    • because type variable 'a' would escape its scope
    This (rigid, skolem) type variable is bound by
      a pattern with constructor: T :: forall b a. a -> (a -> b) -> T b,
      in a pattern binding
      at <interactive>:25:12-16
    • In the pattern: T a f
      In a pattern binding: T a f = t
      In the expression: let T a f = t in f a

結局よくわからんですが．

caseBarと`whereBar`を追加で試してみました．ドキュメントの通り，`caseBar`についてはエラーにならず，`whereBar`は同様のエラーが出ます．

caseBar :: AnyBar b -> b
caseBar ab = case ab of AnyBar x f -> f x

whereBar :: AnyBar b -> b
whereBar ab = f x where AnyBar x f = ab

caseとletはそもそも意味論が違うので、「正気とは思えない」というのは言い過ぎでは……？GADTsや存在型の型推論をモジュラーかつ完全に扱う上では、letやwhereの節は単相的に推論されるほうが都合が良く、またlet式は最適化の過程で式の内側にfloatしたりするのでcaseとは違う扱いが必要になります。正格性の上でも違うものとして扱われていたりして、この辺りの事情を考えるとそれほど「正気ではない」というほどではないんじゃないかと。

すみません、上の文章書いたあと色々見に行って言い過ぎっぽいとまでは思ったけど訂正できるほど理解してもいないのでごめんなさいしか言えないという、この…。

caseは文字通りcase-splittingのための機構で、GADTsによって導入される存在変数をスコープに入れてくれるんですが、letやwhereは第一義的には局所定義のための構文にすぎないんですよね。で、たまたまHaskellが（caseとはぼ同じ意味を持つ引数に対するパターンマッチとは別に）束縛変数そのもののパターンマッチを構文糖衣として許しているために通常の場合はcaseと同じように使えるけれども、存在変数が絡んでくるとそこの違いが現れてくるーーというふうに理解するのがわかりやすいですかね

letBarはcaseBarに簡単にエラボレーションできるし、一般にlet式内のpattern-bindingはcase式にエラボレーションできるので意味論的にはcaseBarが型検査器に通って、letBarが通らない理由はないと思います。
理由はむしろ

Type-checking binding groups is already a nightmare without existentials complicating the picture

や

Also an existential pattern binding at the top level of a module doesn’t make sense, because it’s not clear how to prevent the existentially-quantified type “escaping”

にあって、HaskellのASTではトップレベルの関数束縛とlet式内の関数束縛を区別していないので、結果的にletBarが型検査に通らないのだと思います。

「簡単に」というにはわりと strictness analysis が絡んでくるのでどうなんだろうという気もします．

letBar ab = let !(AnyBar x f) = ab in f x

なら容易に caseBar にエラボレートできるのはそうですけど．

@gksato
評価戦略は型検査時には関係がないと思います。
実際、

letBar ab = let !(AnyBar x f) = ab in f x

を

caseBar ab = case ab of !(AnyBar x f) -> f x

に書き換えても型検査には影響しないので、例えばこのcaseBarを型検査した後にletBarに戻せば、評価規則を含めた動的意味論には影響しません。
書き換えるというのは、実際に実装で書き換える必要はありません。

今の返信中に２回現れる !(AnyBar x f) に ! がついている理由がよくわかっていません．私の意図としては，

foo1 :: (Int, Int) -> Int
foo1 p = let (!x,!y) = (*2) `bimap` (*2) $ p
         in somefunc x y

は，定義上

foo1' :: (Int, Int) -> Int
foo1' p = let q = (*2) `bimap` (*2) $ p
              x = case q of (!x,!_) -> x
              y = case q of (!_,!y) -> y
          in somefunc x y

と等価であるように定義されているのであって，

foo2 :: (Int, Int) -> Int
foo2 p = case (*2) `bimap` (*2) $ p of
  (!x, !y) -> somefunc x y

と等価なのは

foo2' :: (Int, Int) -> Int
foo2' p = let !(!x,!y) = (*2) `bimap` (*2) $ p
          in somefunc x y

なので，それと揃えるならば

letBar1, letBar2, caseBar :: AnyBar b -> b
letBar1 ab = let AnyBar x f = ab in f x
letBar2 ab = let !(AnyBar x f) = ab in f x
caseBar ab = case ab of AnyBar x f -> f x

のうちで，完全に等価であるように定義できそうなのは letBar2 と caseBar だけだよね，ということです．
であるので，「実行中の意味論は異なるが，型検査中だけ適宜 case とみなせばよい」という話だとすれば，最初から等価にできるかも，と言っている letBar2 と caseBar を持ち出している理由がよくわかっていません．

@gksato
すみません。読み違えていました。
上のメッセージの「実際」以降は無視してください。