How do I use GDP to subtype my data types?

Learn
#1

Let’s say I have a type Re a with two features which I call Unsupported.

{-# LANGUAGE GADTs           #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeOperators   #-}

import GDP

data Re a =
      Eps
    | Char a
    | Concat (Re a) (Re a)
    | Union (Re a) (Re a)
    | Star (Re a)
    | UnsupportedA (Re a)
    | UnsupportedB (Re a)

unsafeSupportedEval :: [a] -> Re a -> Bool
unsafeSupportedEval = undefined

I want to use the GDP library to make sure that when I use this unsafe function, I have a proof that the regex being used is checked to be safe. So I start doing this:

hasUnsupported :: Re a -> Bool
hasUnsupported Eps = False
hasUnsupported (Char _) = False
hasUnsupported (Concat r1 r2) = hasUnsupported r1 || hasUnsupported r2
hasUnsupported (Union r1 r2) = hasUnsupported r1 || hasUnsupported r2
hasUnsupported (Star r) = hasUnsupported r
hasUnsupported (UnsupportedA _) = True
hasUnsupported (UnsupportedB _) = True

And then, I bring in some magic incantations

newtype Unsupported re = Unsupported Defn
type role Unsupported nominal

classifySupported :: (Re a ~~ re) ->  Either (Proof (Unsupported re)) (Proof (Not (Unsupported re)))
classifySupported (The re)
    | hasUnsupported re = Left axiom
    | otherwise = Right axiom

Question 1: What is nominal?
Question 2: Is this the correct signature for the function I want for reflection? I can think of some other alternatives. For example,

(Re a ~~ re) ->  Proof (Unsupported re || Not (Unsupported re))

Or, Re a -> Either ((Re a) ?Unsupported) ((Re a) ? (Not Unsupported))

Question 3: The second option is a kind mismatch. What should be the correct way to use the Not operation?

I can have a function which only deals with the subtype of Unsupported things.

withUnsupported :: (Re a ? Unsupported) -> IO ()
withUnsupported (The re) = case re of
    UnsupportedA _ -> putStrLn "UnsupportedA"
    UnsupportedB _ -> putStrLn "UnsupportedB"

This looks fine to me?

Question 4: How do I write something similar for supported? withSupported :: (Re a ? (Not Unsupported)) -> IO ()

Question 5: How do invoke withUnsupported correctly in the following function? I want to be able to combine the proof with the re.

useRe :: Re a -> IO ()
useRe re = case classifySupported (The re) of
    Left unsupported -> withUnsupported undefined -- how do I define this?
    Right supported -> do
        putStrLn "Supported"
        print $ unsafeSupportedEval "abc" re
1 Like
#2

Question 2: Is this the correct signature for the function I want for reflection? I can think of some other alternatives. For example,

Your first version of classifySupported is the right one.

classifySupported :: (Re a ~~ re) ->  Either (Proof (Unsupported re)) (Proof (Not :.: (Unsupported re)))

You do not want the result to be Proof (Unsupported re || Not (Unsupported re)) instead, because then there is no way to tell which clause is true. That’s really the same as returning Proof True.

And you do not want Re a -> Either ((Re a) ? Unsupported) ((Re a) ? (Not :.: Unsupported)) because it could return a different regex than the one you provided. (See next question for (:.:).)

Question 3: The second option is a kind mismatch. What should be the correct way to use the Not operation?

You need a composition operator.

data (:.:) f g x

compose :: Proof (f (g x)) -> Proof ((f :.: g) x)
compose _ = axiom

uncompose :: Proof ((f :.: g) x) -> Proof (f (g x))
uncompose _ = axiom

So you can write the predicate Not :.: Unsupported.

Question 4: How do I write something similar for supported? withSupported :: (Re a ? (Not Unsupported)) -> IO ()

You can just write a partial function that errors out in unsupported cases. If users use your library safely (i.e., without access to internals), those cases should not happen. But the type system is not powerful enough to let you as a library writer make use of that fact.

Question 5: How do invoke withUnsupported correctly in the following function? I want to be able to combine the proof with the re.

useRe :: Re a -> IO ()
useRe = name $ \re -> case classifySupported re of
    Left unsupported -> withUnsupported (unname (re ... unsupported))
    Right supported -> withSupported (unname (re ... compose supported))

-- with these signatures
withUnsupported :: Re a ? Unsupported -> IO ()
withSupported :: Re a ? (Not :.: Unsupported) -> IO ()

It may help to ignore ? at first. You can do a lot with only ~~ and Proof.

useRe :: Re a -> IO ()
useRe = name $ \re -> case classifySupported re of
    Left unsupported -> withUnsupported re unsupported
    Right supported -> withSupported re supported

-- with these signatures
withUnsupported :: Re a ~~ re -> Proof (Unsupported re) -> IO ()
withSupported :: Re a ~~ re -> Proof (Not (Unsupported re)) -> IO ()

Question 1: What is nominal?

By default the inferred role here would be phantom, which means you can always coerce :: Unsupported re1 -> Unsupported re2 for any re1 or re2. If we consider a value x :: Unsupported re as evidence that the regex re is unsupported, then coerce could turn it into evidence that any other regex is unsupported. The nominal role prevents that.

-- F phantom
coerce :: F a -> F b

-- F representational
coerce :: Coercible a b => F a -> F b

-- F nominal
coerce :: F a -> F a

But unless I’m missing something, you can define new predicates (like Unsupported or (:.:)) as empty types and not worry about roles. They are only ever used as parameters of Proof (or ::: or Satisfy) so their values don’t matter.

2 Likes
#3

Thanks for this reply.

When I try the following

I get this error:

    • Expecting one more argument to ‘f’
      Expected a type, but ‘f’ has kind ‘k3 -> k2’
    • In the first argument of ‘(:.:)’, namely ‘f’
      In the first argument of ‘Proof’, namely ‘((f :.: g) x)’
      In the type signature:
        compose :: Proof (f (g x)) -> Proof ((f :.: g) x)
   |
20 | compose :: Proof (f (g x)) -> Proof ((f :.: g) x)
   |                                       ^

Also, it appears that compose and uncompose exhibit an isomorphism between the Proofs of f (g x) and (f :.: g) x. Why not establish an isomporphism between the types themselves rather than their Proofs?

Why isn’t the composition operation part of the GDP library?

1 Like
#4

My bad, (:.:) should be defined with explicit kinds.

data (:.:) (f :: k -> Type) (g :: l -> k) (x :: l)

Why not establish an isomorphism between the types themselves rather than their Proofs?

The arguments of Proof are morally not types. GDP uses Type as an extensible type-level data type to symbolically represent logical propositions, using data to declare new Type constructors. Such a constructor doesn’t have inherent meaning, instead its meaning is defined by the functions for consuming or producing Proofs that are exposed to users.

It’s possible to do an alternative version of GDP where types are used as propositions, but you would lose the ability of erasing proofs so they have no run-time cost.

1 Like