Skip to content

Instantly share code, notes, and snippets.

@pasberth
Created June 21, 2015 18:05
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save pasberth/4391e1ed5af7e51f8903 to your computer and use it in GitHub Desktop.
ExistentialQuantification by Rank2Types

存在型をλ式にエンコードする件について

Haskellには存在型というものがある。 これを使うとヘテロリストなどがつくれる例。

{-# LANGUAGE ExistentialQuantification  #-}
data T = forall t. Mk t
xs :: [T]
xs = [Mk 42, Mk "answer"]

ここで疑問が浮かぶ。このデータ型はλ式にエンコードできるのか? ということだ。その方法は Rank2Types を使うことである。

{-# LANGUAGE Rank2Types #-}
type T a = (forall t. t -> a) -> a
mk :: a -> T b
mk x = \f -> f x
xs :: [T a]
xs = [mk 42, mk "answer"]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment