、この<a href="https://github.com/kosmikus/SSGEP/blob/master/LectureNotes.pdf">paper</a>で

Question

FORALL使用して1次のシグネチャを持つ関数があります：

vreplicate :: forall a n . SNatI n => a -> Vec a n 

この署名とforallを持っていないものの違いは何ですか。

vreplicate :: SNatI n => a -> Vec a n 

？私は、forallがないと暗黙のうちに、全ての型変数に名前をつけるのにはforallがあることを暗示しているという印象を受けました。

Answer 1

forallを含む重要なケースが2つあります。 1つは、forallの位置が型の意味を変えることができるということです。矢印の左側にある場合、それは関数の引数が他のものよりも多相であることを意味します。この違いは基本的な違いです。ただし、ここでは適用されないようです。

第差が構文（よりむしろ基本的な）ものである、即ち：暗黙forallずにバインドされた変数がない一方ScopedTypeVariablesの存在下で、forallによって結合変数は、タイピングスコープを開きます。したがって、vreplicateの本体では、型変数aとnを使用できます。また、それらがの署名で言及されているのと同じ型を参照していることを確かめてください。 forall（またはScopedTypeVariablesなし）がなければ、新鮮普遍的に定量化された変数を導入するvreplicateのボディにaとnの使用、およびその場合、彼らはvreplicateの署名内の型で統一されたことを確認するためにプログラマの責任だろう望んでいた。詳細はthe documentationで入手できます。

紙を注意深く読まないと、私は確信が持てませんが、後者がここで起こっていると確信しています。