haskell-ja > Archives > 2016/04/10

第7回 「プログラミング言語の基礎概念」読書会 #heyhey_haskell http://sampou.connpass.com/event/29344/
で出た健全ではない論証の例をHaskellで書いていて気付いたのですが、HaskellのEmptyCases拡張を使うとあらゆるものの否定が証明できてしまうように見えるのですが、EmptyCases拡張のバグだったりしないのかなぁ。

data Absurd
type Not a = a -> Absurd
strange :: Not a
strange a = case a of { }

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE EmptyCase #-}

module TypeLevelProgramming
       where

data Absurd
type Not a = a -> Absurd

data Animal = Bird | Pig

data SAnimal (a :: Animal) where
  SBird :: SAnimal Bird
  SPig  :: SAnimal Pig

data CanFly (a :: Animal) where
  BirdCanFly :: CanFly Bird

statement :: (forall a . SAnimal a -> CanFly a) -> CanFly Pig
statement prp = prp SPig

strange :: Not (CanFly Bird)
strange birdcanfly = case birdcanfly of {}

pig_cannot_fly :: Not (CanFly Pig)
pig_cannot_fly canfly = case canfly of { }