Skip to content

Instantly share code, notes, and snippets.

@stedolan

stedolan/Injective.hs

Last active March 26, 2024 17:44
Download ZIP

Revisions

  1. stedolan revised this gist Mar 26, 2024. 1 changed file with 3 additions and 9 deletions.
    12 changes: 3 additions & 9 deletions Injective.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -6,21 +6,15 @@

    data False

    data Equ (a :: *) (b :: *) where
    Refl :: Equ a a

    data I (f :: * -> *) where

    injCast :: Equ (I x) (I y) -> x a -> y a
    injCast Refl p = p

    data P (x :: *) where
    MkP :: Equ x (I a) -> (a x -> False) -> P x
    MkP :: (a (I a) -> False) -> P (I a)

    falsePIP :: P (I P) -> False
    falsePIP h@(MkP eq np) = np (injCast eq h)
    falsePIP h@(MkP np) = np h

    false :: a
    false = case falsePIP (MkP Refl falsePIP) of {}
    false = case falsePIP (MkP falsePIP) of {}

    main = putStrLn false
  2. stedolan created this gist Mar 26, 2024.
    26 changes: 26 additions & 0 deletions Injective.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,26 @@
    {-# LANGUAGE GADTs #-}
    -- nontermination without any recursion, even in types
    -- possible because of impredicativity + injectivity
    -- based on https://gist.github.com/leodemoura/0c88341bb585bf9a72e6
    -- see also https://github.com/idris-lang/Idris-dev/issues/3687

    data False

    data Equ (a :: *) (b :: *) where
    Refl :: Equ a a

    data I (f :: * -> *) where

    injCast :: Equ (I x) (I y) -> x a -> y a
    injCast Refl p = p

    data P (x :: *) where
    MkP :: Equ x (I a) -> (a x -> False) -> P x

    falsePIP :: P (I P) -> False
    falsePIP h@(MkP eq np) = np (injCast eq h)

    false :: a
    false = case falsePIP (MkP Refl falsePIP) of {}

    main = putStrLn false