YoshikuniJujo on Nostr: data Foo t where Foo :: a -> b -> Foo (a -> b) ...

data Foo t where
Foo :: a -> b -> Foo (a -> b)

みたいな型ってすこし不思議な感じがある。型の足し算と引き算の結果がおかしいような気がする。

Foo True 'c' :: Foo (Bool -> Char)

けど、たとえば

foo :: Foo (Bool -> Char) -> Bool -> Char
foo (Foo b0 c) b
| b == b0 = c
| otherwise = 'd'

みたいな関数を定義できるので、それほどおかしくもないのかもしれない。

a -> a -> bみたいな関数を使うことで、(+ 1)を(- 1)に変えることができる感じか。