[n] := ∀ X1,...,Xn . X1 + ... + Xn in_n,k :: [n-1] -> [n]
@kazu
N に対して、EvenNumbers E を N のsubtype としてユーザーが定義したいような状況です。λ> m x = x x
<interactive>:1:10: error: • Occurs check: cannot construct the infinite type: t ~ t -> t1 • In the first argument of 'x', namely 'x' In the expression: x x In an equation for 'm': m x = x x • Relevant bindings include x :: t -> t1 (bound at <interactive>:1:3) m :: (t -> t1) -> t1 (bound at <interactive>:1:1)
> m m
[T] = T
なお、ACM 会員には ACM DL への無制限のアクセスが付与されるようです。年 $198 で入れるのかな？)そのとおりです。私も会員です。DLへのアクセスはオプション？扱いでこれが要らなければ半額になります。DLへの無制限アクセスがなくても、CACMの電子版にはアクセスできると思います。