Phantom types for crypto keys

Phantom types and GADTs are well-known techniques in Haskell for helping build programs that enforce certain kinds of type refinement: they essentially are used to help serve witness to some type equality. This type equality generally enforces constraints on the nature of your code. In the case of GADTs, your witnesses are the data type constructors (which actually carry around an equality constraint,) and with phantom types, you typically build valid terms from an encapsulated data type, using provided APIs.

While working on salt I recently found the types I used for various key types to be a bit inexpressive. I want the library to be type safe in a way that avoids common misusage, and helps the user write correct code: the API should be explanatory and simple.

My old API looked like this:

newtype PublicKey = PublicKey { unPublicKey :: ByteString } deriving ...
newtype SecretKey = SecretKey { unSecretKey :: ByteString } deriving ...

type KeyPair = (PublicKey, SecretKey)

And then you had things like the public-key encryption API, which looked like:

createKeypair :: IO KeyPair
encrypt :: Nonce       -- Nonce
        -> ByteString  -- Plaintext
        -> PublicKey   -- Receiver public key
        -> SecretKey   -- Sender secret key
        -> ByteString  -- Ciphertext

I thought for a little bit and eventually came up with a key API that is shared for all interfaces, very minimal and a bit more explanatory. I took the idea from repa: to tag the type constructor with type variables, and use them for distinguishing the kind of data.

So the new API looks like this:

newtype Key s i = Key { unKey :: ByteString }

data Public
data Secret

type KeyPair i = (Key Public i, Key Secret i)

And now encryption looks like this:

data PublicEncryptionKey
createKeypair :: IO (KeyPair PublicEncryptionKey)
encrypt :: Nonce
        -> ByteString
        -> Key Public PublicEncryptionKey
        -> Key Secret PublicEncryptionKey
        -> ByteString

The API is a bit wordier, but for the most part, keys will be either parametric in the key types or the key type is fixed for an API, so there’s not too much need to be so specific I imagine.

I actually like this new API quite a bit because it’s easy to see at a glance what a key is for, and type-checking makes sure you won’t make simple mistakes. It’s also quite self-explanatory, I think.

I’m working on reducing the wordiness of imports and the APIs further, so hopefully this can be improved on.

Math test

This is a test of MathJax. $$ \newcommand{\zero}{\mathsf{z}} \newcommand{\succ}[1]{\mathsf{s}({#1})} \newcommand{\iter}[4]{\mathsf{iter}({#1}, \zero \to {#2}, \succ{#3} \to {#4})} \begin{array}{lcl} A & ::= & 1 \bnfalt A \times B \bnfalt A \to B \bnfalt \N \\ e & ::= & () \bnfalt (e, e) \bnfalt \fst{e} \bnfalt \snd{e} \bnfalt \fun{x}{e} \bnfalt e \; e' \\ & | & \zero \bnfalt \succ{e} \bnfalt \iter{e}{e_z}{x}{e_s} \bnfalt x \bnfalt e : A \\ \Gamma & ::= & \cdot \bnfalt \Gamma, x:A \end{array} $$ $$ \begin{array}{cc} \frac{ x:A \in \Gamma } { \judge{\Gamma}{x}{A} } & \frac{ } {\judge{\Gamma}{()}{1}} \\[1em] \frac{\judge{\Gamma}{e_1}{A_1} \qquad \judge{\Gamma}{e_2}{A_2}} {\judge{\Gamma}{(e_1, e_2)}{A_1 \times A_2}} & \frac{\judge{\Gamma}{e}{A_1 \times A_2}} {\judge{\Gamma}{\pi_i(e)}{A_i}} \\[1em] \frac{\judge{\Gamma, x:A}{e}{B}} {\judge{\Gamma}{\fun{x}{e}}{A \to B}} & \frac{\judge{\Gamma}{e}{A \to B} \qquad \judge{\Gamma}{e'}{A}} {\judge{\Gamma}{e\;e'}{B}} \\[1em] \frac{ } {\judge{\Gamma}{\zero}{\N}} & \frac{\judge{\Gamma}{e}{\N} } {\judge{\Gamma}{\succ{e}}{\N}} \\[1em] \frac{\begin{array}{l} \judge{\Gamma}{e}{\N} \\ \judge{\Gamma}{e_z}{A} \\ \judge{\Gamma, x:A}{e_s}{A} \end{array}} {\judge{\Gamma}{\iter{e}{e_z}{x}{e_s}}{A}} & \frac{\judge{\Gamma}{e}{A}} {\judge{\Gamma}{(e:A)}{A}} \end{array} $$ ​It seems to work!