fork download 
  1. -- ttps://twitter.com/Iceland_jack/status/1033409786044444672
  2. -- ttps://ja.wikibooks.org/wiki/Haskell/%E3%82%AB%E3%83%AA%E3%83%BC%3D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B
  3. -- ttps://gist.github.com/CMCDragonkai/b203769c588caddf8cb051529339635c
  4.  
  5. {-# OPTIONS_GHC -Wall #-}
  6. {-# LANGUAGE GADTs #-}
  7. {-# LANGUAGE PolyKinds #-}
  8. {-# LANGUAGE RankNTypes #-}
  9. {-# LANGUAGE ScopedTypeVariables #-}
  10.  
  11. import Data.Functor.Compose (Compose(..))
  12. import Data.Kind (Type)
  13. import Data.Void (Void)
  14.  
  15. main :: IO ()
  16. main = putStrLn "カリー=ハワード同型"
  17.  
  18. -- | Exists f ~ exists x. f x
  19. data Exists :: (k -> Type) -> Type where
  20.   Exists :: forall f x. f x -> Exists f
  21.  
  22. -- | Forall f ~ forall x. f x
  23. data Forall :: (k -> Type) -> Type where
  24.   Forall :: forall f. (forall x. f x) -> Forall f
  25.  
  26. -- | ￢P <=> P->⊥
  27. newtype Not a = Not (a -> Void)
  28.  
  29. -- | ∀xP(x) -> ￢[∃x￢P(x)]
  30. forallToExists :: forall p. Forall p -> Not (Exists (Compose Not p))
  31. forallToExists = Not . f where
  32.   f :: Forall p -> Exists (Compose Not p) -> Void
  33.   f (Forall px) (Exists (Compose (Not x))) = x px
  34.  
  35. -- | ∃xP(x) -> ￢[∀x￢P(x)]
  36. existsToForall :: forall p. Exists p -> Not (Forall (Compose Not p))
  37. existsToForall = Not . f where
  38.   f :: Exists p -> Forall (Compose Not p) -> Void
  39.   f (Exists px) (Forall (Compose (Not x))) = x px
  40.  
Success #stdin #stdout 0s 0KB
comments (?)
stdin 
Standard input is empty
stdout 
カリー=ハワード同型
https://ideone.com/RSvVYo
language:
Haskell (ghc 8.4.4)
created:
5 years ago
visibility:
secret

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!