型レベルの何か

apply (undefined :: n -> Succ (Succ n)) Zero :: Succ (Succ Zero)

型レベルのλ (System FのΛ)があったらいいのにーという風に理解したのですがそりゃ難しそうに思えます．

難しくありませんでした．何かそれっぽいのができました．知りもしないのに適当なこと言ってすみません

コード

{-# OPTIONS -fglasgow-exts #-}
{-# LANGUAGE UndecidableInstances, OverlappingInstances, IncoherentInstances, NoMonomorphismRestriction #-}

data Succ n = Succ n; data Zero = Zero

class Apply f x x' | f x -> x' where
  apply :: f -> x -> x'

instance a ~ a' => Apply (a -> b) a' b where
  apply f = f

succ = apply Succ

succsucc = apply (Succ . Succ)

試す

Main> :t succsucc
succsucc :: a -> Succ (Succ a)
Main> :t apply (undefined :: n -> Succ (Succ n))
apply (undefined :: n -> Succ (Succ n)) :: n -> Succ (Succ n)

って、この場合 apply は ($) と何ら変わりはないですね。 何をやりたかったのかよくわからなくなってきた。