encode "exists" from classic logic in Haskell using singletons

exists.md

I was reading through Type Theory and Formal Proofs (recommended by @parsonsmatt), and there was some info about how to represent "exists" (Ǝ).

In the type-theory version of classical logic, "exists" can represented as a higher-order function using "forall" like the following:

Ǝ x : S. P x is defined as ∀ A : *. (∀ x : S. P x -> A) -> A

This is read like the following: "There exists an element x of the set S, where the predicate P holds for x."

(When you're translating to Haskell, you can think of x as a value with type S, and P as a dependently-typed function taking a value x and returning a new type.)

The forall part can be read like the following: "For all types A, if you give me a function that works on ALL x in S where P holds for x and returns some A, then I can give you back an A". Which makes sense, because I can just pass that function the x and P x that I already have.

I wanted to see if I could represent this in Haskell using singletons, so I came up with something like the following:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits
import GHC.Natural

$(singletons [d|
  myTestYo :: Bool -> Nat
  myTestYo True = 1
  myTestYo False = 0
  |])

newtype Exists aKind (f :: aKind ~> bKind) =
  Exists
    ( forall x
    . ( forall (a :: aKind)
      . Sing a
     -> Sing (f @@ a)
     -> x
      )
   -> x
    )

mkExists :: forall aKind (bKind :: Type) (a :: aKind) (f :: aKind ~> bKind). Sing a -> Sing (f @@ a) -> Exists aKind f
mkExists singA singF = Exists $ \func -> func singA singF

test1 :: Exists Bool MyTestYoSym0
test1 = mkExists @Bool @Nat @'True sing sing

test2 :: Exists Bool MyTestYoSym0 -> String
test2 (Exists f) = f go
  where
    go :: forall (a :: Bool). Sing a -> Sing (MyTestYoSym0 @@ a) -> String
    go STrue singF = "got a true singleton, and the predicate is: " <> show singF
    go SFalse singF = "got a false singleton, and the predicate is: " <> show singF

test3 :: String
test3 = test2 test1

test4 :: Exists Bool MyTestYoSym0 -> Natural
test4 (Exists f) = f go
  where
    go :: forall (a :: Bool). Sing a -> Sing (MyTestYoSym0 @@ a) -> Natural
    go STrue (singF :: Sing 1) = 1
    go SFalse (singF :: Sing 0) = 0

test5 :: Natural
test5 = test4 test1

test1 says that there exists some x :: Bool and the predicate MyTestYo takes x (and returns a Nat, which you can figure out by the kind of MyTestYo). Then test2 makes use of that by showing the resulting Nat.

This file can be loaded with GHCi in the following environment:

$ nix-shell -p "haskell.packages.ghc844.ghcWithPackages (pkgs: with pkgs; [singletons])"