_TZ_16934-euclid.tex

\documentclass[format=sigplan, review=false, screen=true]{acmart}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{fontspec}
\setmonofont[
  Contextuals={Alternate},
  Scale=0.9
]{Fira Code}
\makeatletter
\def\verbatim@nolig@list{}
\makeatother

\usepackage{booktabs} % For formal tables
\usepackage{bussproofs}
\usepackage{graphics}
\usepackage{xcolor}

\usepackage{minted}
\usemintedstyle{friendly}
\setminted{
    frame=lines,
    framesep=2mm,
    baselinestretch=1.2,
    %bgcolor=lightgray,
    fontsize=\footnotesize
    }

\usepackage{filecontents}

\usepackage[ruled]{algorithm2e} % For algorithms
\renewcommand{\algorithmcfname}{ALGORITHM}
\SetAlFnt{\small}
\SetAlCapFnt{\small}
\SetAlCapNameFnt{\small}
\SetAlCapHSkip{0pt}
\IncMargin{-\parindent}

\usepackage{listings}
\lstdefinestyle{mystyle}{
    %backgroundcolor=\color{backcolour},   
    commentstyle=\color{gray},
    keywordstyle=\color{blue},
    numberstyle=\tiny,
    stringstyle=\color{purple},
    basicstyle=\small\tt,
    breakatwhitespace=false,         
    breaklines=true,                 
    captionpos=b,                    
    keepspaces=true,                 
    %numbers=left,                    
    numbersep=5pt,                  
    showspaces=false,                
    showstringspaces=false,
    showtabs=false,
    frame=single,
    xleftmargin=1em,
    xrightmargin=1em,
    frame=shadowbox,
    rulesepcolor=\color{gray},
    tabsize=2
}
 
\lstset{style=mystyle,
  literate=
  {->} {$\to$} 2
  {<-} {$\leftarrow$} 2
  {=>} {$\Rightarrow$} 2
  {forall} {$\forall$} 1
  {exists} {$\exists$} 1
  {phi} {$\varphi$} 1
  {rho} {$\rho$} 1
  {kappa} {$\kappa$} 1
  {$nu$} {$\nu$} 1
  {$mu$} {$\mu$} 1
  {gamma} {$\gamma$} 1
  {subsetX} {$\subset$} 1
  {~>} {$\rightsquigarrow$} 2
  {<~>} {$\leftrightsquigarrow$} 3
  {elem} {$\in$} 1
}

% Metadata Information
\acmJournal{TWEB}
\acmVolume{9}
\acmNumber{4}
\acmArticle{39}
\acmYear{2018}
\acmMonth{3}
\copyrightyear{2018}
%\acmArticleSeq{9}

% Copyright
%\setcopyright{acmcopyright}
\setcopyright{acmlicensed}
%\setcopyright{rightsretained}
%\setcopyright{usgov}
%\setcopyright{usgovmixed}
%\setcopyright{cagov}
%\setcopyright{cagovmixed}

% DOI
\acmDOI{0000001.0000001}

% Paper history
\received{June 2018}
%\received[revised]{March 2009}
%\received[accepted]{June 2009}

% Document starts
\begin{document}
% Title portion. Note the short title for running heads
\title[Ghosts of Departed Proofs]{Functional Pearl: Ghosts of Departed Proofs}

\author{Matt Noonan}
\orcid{1234-5678-9012-3456}
\affiliation{%
  \institution{Kataskeue LLC}
%  \streetaddress{Esty St}
  \city{Ithaca}
  \state{NY}
  \postcode{14850}
  \country{USA}}
\email{mnoonan@kataskeue.com}


\begin{abstract}

  We present a simple technique that allows library authors to
  control how APIs are used.

\end{abstract}


%
% The code below should be generated by the tool at
% http://dl.acm.org/ccs.cfm
% Please copy and paste the code instead of the example below.
%
\begin{CCSXML}
<ccs2012>
 <concept>
  <concept_id>10010520.10010553.10010562</concept_id>
  <concept_desc>Computer systems organization~Embedded systems</concept_desc>
  <concept_significance>500</concept_significance>
 </concept>
 <concept>
  <concept_id>10010520.10010575.10010755</concept_id>
  <concept_desc>Computer systems organization~Redundancy</concept_desc>
  <concept_significance>300</concept_significance>
 </concept>
 <concept>
  <concept_id>10010520.10010553.10010554</concept_id>
  <concept_desc>Computer systems organization~Robotics</concept_desc>
  <concept_significance>100</concept_significance>
 </concept>
 <concept>
  <concept_id>10003033.10003083.10003095</concept_id>
  <concept_desc>Networks~Network reliability</concept_desc>
  <concept_significance>100</concept_significance>
 </concept>
</ccs2012>
\end{CCSXML}

\ccsdesc[500]{Computer systems organization~Embedded systems}
\ccsdesc[300]{Computer systems organization~Redundancy}
\ccsdesc{Computer systems organization~Robotics}
\ccsdesc[100]{Networks~Network reliability}

%
% End generated code
%


\keywords{Wireless sensor networks, media access control,
multi-channel, radio interference, time synchronization}




\maketitle

% The default list of authors is too long for headers.
\renewcommand{\shortauthors}{M. Noonan}

%\input{samplebody-journals}

\section{Introduction}

\subsection{Encoding with Universals}

It is a theorem of both classical and constructive logics that
\[\forall t.~ (\forall s. \varphi(s) \Rightarrow t) \Rightarrow t \equiv \exists c.~ \varphi(c)\]

\section{Warmup: Not quite dependent types}

\begin{filecontents*}{ex1.hs}  
{-# LANGUAGE RankNTypes #-}
module Sized
  (Size, the, sZipWith, sizing, align) where

newtype Size n a = Size a

the :: Size n a -> a
the (Size x) = x

sZipWith :: (a -> b -> c)
         -> Size n [a]
         -> Size n [b]
         -> Size n [c]
sZipWith f xs ys =
  Size (zipWith f (the xs) (the ys))
  
sizing :: [a] -> (forall n. Size n [a] -> t) -> t
sizing xs k = k (Size xs)

align :: Size n [a] -> [b] -> Maybe (Size n [b])
align xs ys = if length (the xs) == length ys
              then Just (Size ys)
              else Nothing

\end{filecontents*}

\begin{filecontents*}{ex2.hs}
import Sized

dot :: Size n [Double] -> Size n [Double] -> Double
dot xs ys = sum (the $ sZipWith (*) xs ys)

main :: IO ()
main = do
  xs <- readLn
  ys <- readLn
  sizing xs $ \xs' -> do
    case align xs' ys of
      Nothing  -> putStrLn "Size mismatch!"
      Just ys' -> print (dot xs' ys')
\end{filecontents*}

\begin{figure}
    \inputminted{haskell}{ex1.hs}
  \caption{A small module defining a type for lists with a known length.}
\end{figure}
\begin{figure}
    \inputminted{haskell}{ex2.hs}
    \caption{A user-defined dot product function that can only be used on same-sized lists,
    and a usage example.}
\end{figure}


\begin{lstlisting}[language=Haskell]
  norm2 :: [Double] -> Double
  norm2 xs = sizing xs (\v -> v `dot` v)
\end{lstlisting}

\begin{lstlisting}[language=Haskell]
  sizing xs $ \xs' -> 
    case align xs' ys of
      Just ys' -> (xs' `dot` ys') / (xs' `dot` xs')
      Nothing  -> 17
\end{lstlisting}

Despite  • appearences, the phantom type parameter $n$ does not really represent the vector's length
{\em per se}. Instead, we propose to think of \texttt{Size n} as a predicate, and values of
type \texttt{Size n [a]} should be thought of as ``lists of type \texttt{[a]}, equipped with a proof
that they satisfy \texttt{Size n}''. Critically, this proof has no run-time impact: it is trapped in
the phantom type parameter.

This approach gives us a straightforward way to interpret the type signatures from example ***:

\begin{lstlisting}[language=Haskell]
  -- You can take the dot product of two lists, if you have proven
  -- that they have the same Size n.
  dot :: Size n [Double] -> Size n [Double] -> Double

  -- When you map a function over a list of Size n, the
  -- result will also have Size n.
  smap :: (a -> b) -> Size n [a] -> Size n [b]

  -- For any list, there is some n such that Size n is true.
  sizing :: [a] -> (forall n. Size n [a] -> t) -> t

  -- Given a list of Size n, we may be able to prove that
  -- another list also has Size n.
  align :: Size n [a] -> [b] -> Maybe (Size n [b])
\end{lstlisting}

As we attach increasingly sophisticated information into the phantom types, it becomes useful to
have a uniform method for \emph{forgetting} all of the ornamentation, revealing the normal
value underneath.

\begin{filecontents*}{theTC.hs}
class The d a | d -> a where
    the :: d -> a
    default the :: Coercible d a => d -> a
    the = coerce
    
instance The (Size n a) a
\end{filecontents*}

\begin{figure}
  \inputminted{haskell}{theTC.hs}
  \caption{The \texttt{The} typeclass, for dropping ghosts
    from a type. The default instance should always be used,
    so new instances can be created with an empty
    \texttt{instance} declaration.}
\end{figure}

\section{Case Study \#1: Sorted lists}

\begin{filecontents*}{named.hs}
module Named (Named, name) where

import The

newtype Named name a = Named a
instance The (Named name a) a

name :: a -> (forall name. Named name a -> t) -> t
name x k = k (coerce x)
\end{filecontents*}

\begin{filecontents*}{ordered.hs}
module Sorted
  (Named, SortedBy, sortBy, mergeBy) where   

import The
import Named

import qualified Data.List as L
import qualified Data.List.Utils as U

newtype SortedBy o a = SortedBy a
instance The (SortedBy o a) a
  
sortBy :: Named comp (a -> a -> Ordering)
       -> [a]
       -> SortedBy comp [a]
sortBy comp xs = coerce (L.sortBy (the comp) xs)

mergeBy :: Named comp (a -> a -> Ordering)
        -> SortedBy comp [a]
        -> SortedBy comp [a]
        -> SortedBy comp [a]
mergeBy comp xs ys =
  coerce (U.mergeBy (the comp) (the xs) (the ys))        
\end{filecontents*}

\begin{filecontents*}{usageO.hs}
import Sorted
import Named
main = do
  xs <- readLn :: IO Int
  ys <- readLn
  name (>) $ \gt -> do
    let xs' = sortBy gt xs
        ys' = sortBy gt ys
    print (the xs', the ys', the (mergeBy gt xs' ys'))
\end{filecontents*}

\begin{figure}
  \inputminted{haskell}{ordered.hs}
  \caption{A module for working with lists that have been sorted by an arbitrary
    comparator.}
\end{figure}


\begin{figure}
  \inputminted{haskell}{named.hs}
  \caption{A module for attaching ghostly names to values.}
\end{figure}

\begin{figure}
  \inputminted{haskell}{usageO.hs}
  \caption{Usage example}
  \end{figure}
Clients of the library are somewhat more restricted, in the sense that they cannot create a
value of type \texttt{OrderedBy comp t} without going through the library's public API.

\begin{minted}{haskell}
minimum_O1 :: SortedBy comp [a] -> Maybe a
minimum_O1 xs = case (the xs) of
    []    -> Nothing
    (x:_) -> Just x
\end{minted}

\subsection{Conjuring a name}

Finally, for the user to be able to \emph{use} this library, there must be a way for
them to create \texttt{Named} values from normal values. The library must export a
function similar to this:

\begin{lstlisting}
name :: a -> (forall name. Named name a -> t) -> t
name x k = k (coerce x)
\end{lstlisting}

This function is quite similar to \texttt{sizing} from the previous section, and the rank-2
type gives it a bit of an ominous feel. You might wonder: why not just have a function
with a simple type like this?

\begin{lstlisting}
any_name :: a -> Named name a
any_name = coerce
\end{lstlisting}

The crux of the issue is all about \emph{who gets to choose} what \texttt{name} will be.
In the signature of \texttt{any\_name}, the \emph{caller} gets to select the types \texttt{a}
and \texttt{name}. In particular, they can attach any name they would like!

If that still does not sound so bad, consider this code:

\begin{minted}{haskell}
up, down :: Named () (Int -> Int -> Ordering)
up = any_name (<)
down = any_name (>)

list1 = sortBy up   [1,2,3]
list2 = sortBy down [1,2,3]

merged :: [Int]
merged = the (mergeBy up list1 list2)
-- [1,2,3,3,2,1]
\end{minted}

Now compare to the analogous program, using \texttt{name} instead of \texttt{any\_name}:
\begin{minted}{haskell}
name (<) $ \up ->
  name (>) $ \down ->
    let list1 = sortBy up   [1,2,3]
        list2 = sortBy down [1,2,3]
    in the (mergeBy up list1 list2)
\end{minted}

resulting in a compile-time error:

\begin{lstlisting}
  • Couldn't match type "name1" with "name"
        ...
    Expected type: SortedBy name [Integer]
      Actual type: SortedBy name1 [Integer]
\end{lstlisting}

A general rule of thumb for library authors is: \emph{a ghost should not appear in the return type,
  unless it also appears in an argument's type}. This simple rule ensures that
the user of the library will not be allowed to materialize ghosts out of thin air.

\section{Case Study \#2: \texttt{Maybe}-free lookup in containers}

\begin{filecontents*}{justified.hs}
newtype Keys φ a = Keys a
instance The (Keys φ a) a

newtype k ∈ φ = Element k
instance The (k ∈ φ) k

member ::  k -> Keys φ (Map k v) -> Maybe (k ∈ φ)

lookup   :: (k ∈ φ) -> Keys φ (Map k v) -> v

reinsert :: (k ∈ φ) -> v -> Keys φ (Map k v) -> Keys φ (Map k v)

vmap     :: (a -> b) -> Keys φ (Map k a) -> Keys φ (Map k b)

withMap  :: Map k v  -> (forall φ. (Keys φ (Map k v) -> t) -> t)
\end{filecontents*}

\begin{lstlisting}[language=Haskell]
test_table = Map.fromList [ (1, "Hello")
                          , (2, "world!") ]

withMap test_table $ \table ->
  case member 1 table of
 
    Nothing  -> putStrLn "Missing key!"
  
    Just key -> do
      -- We have proven that the key is
      -- present, and can now use it
      -- Maybe-free...
      putStrLn ("Found key: "     ++ show key)
      putStrLn ("Value in map 1: " ++
                lookup key table)
      
      -- ...even in certain other maps!
      let table'  = reinsert key "Howdy" table
          table'' = fmap (map upper) table
      putStrLn ("Value in map 2: " ++
                lookup key table')
      putStrLn ("Value in map 3: " ++
                lookup key table'')
{- Output:
Found key: JKey 1
Value in map 1: Hello
Value in map 2: Howdy
Value in map 3: HELLO
-}       
\end{lstlisting}

\subsection{Application: a type for directed graphs}

\begin{lstlisting}[language=Haskell]
data Neighbors phi = Neighbors
    { outEdges :: [Vertex elem phi]
    , inEdges  :: [Vertex elem phi] }
  
type Digraph phi = Keys phi (Map Vertex (Neighbors phi))
\end{lstlisting}

\begin{lstlisting}[language=Haskell]
addEdge   :: Vertex phi -> Vertex phi -> (forall phi'. Digraph phi -> t) -> t
\end{lstlisting}


\begin{lstlisting}[language=Haskell]
check :: Int -> Digraph phi -> Either (FreshVertex phi) (Vertex phi)
fresh :: Digraph phi -> FreshVertex phi
addVertex :: FreshVertex phi -> Digraph phi ->
            (forall phi'. (Vertex phi', Vertex phi -> Vertex phi', Digraph phi') -> t) -> t
\end{lstlisting}

\subsection{Faster lookup}
Although \texttt{justified-containers} defines a simple \texttt{newtype} wrapper for
the key-plus-phantom-proof type, more interesting information about the location of
the key within the corresponding data structure can sometimes be attached.

For example, imagine a simple binary search tree backed by a vector of key-value pairs.
As in the previous example, we will give the \texttt{BST} type a phantom parameter that
represents the set of valid keys present in the tree. But instead of wrapping the key
type directly, we will use an index-plus-phantom-proof representation for keys.

\begin{lstlisting}[language=Haskell]
newtype BST phi k v = BST (Vector (k,v))
newtype Index phi   = Index Int

toBST :: Ord k => Vector (k,v) -> BST phi k v

find   :: Ord k => k -> BST phi k v -> Maybe (Index phi)
access :: Index phi -> BST phi k v -> (k,v)
\end{lstlisting}

\section{Case Study \#3: Encoding arbitrary properties}

\begin{figure*}
  \hspace{-2.5in}
  \scalebox{0.6}{{
  \begin{minipage}{\textwidth}
    \begin{prooftree}
      \AxiomC{}
      \RightLabel{\scriptsize (p)}\UnaryInfC{$\texttt{IsNil}(x) \wedge |x| = 0$}
      \UnaryInfC{$|x| = 0$}
      \UnaryInfC{$0 = |x|$}
      \AxiomC{}
      \RightLabel{\scriptsize (eq)}\UnaryInfC{$|x| = 1 + n$}
      \BinaryInfC{$0 = 1 + n$}
      \AxiomC{}
      \UnaryInfC{$\forall m.~ \neg (0 = 1 + m)$}
      \UnaryInfC{$\neg (0 = 1 + n)$}
      \BinaryInfC{$\bot$}
      \UnaryInfC{$\texttt{IsCons}(x)$}
      \RightLabel{\scriptsize (p)}\UnaryInfC{$\texttt{IsNil}(x) \wedge |x| = 0 \longrightarrow \texttt{IsCons}(x)$}
      \AxiomC{}
      \RightLabel{\scriptsize (q)}\UnaryInfC{$\texttt{IsCons}(x) \wedge |x| = 1 + |\texttt{Tail}(x)|$}
      \UnaryInfC{$\texttt{IsCons}(x)$}
      \RightLabel{\scriptsize (q)}\UnaryInfC{$\texttt{IsCons}(x) \wedge |x| = 1 + |\texttt{Tail}(x)| \longrightarrow \texttt{IsCons}(x)$}
      \AxiomC{}\UnaryInfC{$(\texttt{IsNil}(x) \wedge |x| = 0) \vee (\texttt{IsCons}(x) \wedge |x| = 1 + |\texttt{Tail}(x)|)$}
      \TrinaryInfC{$\texttt{IsCons}(x)$}
      \RightLabel{\scriptsize (eq)}\UnaryInfC{$|x| = 1 + n \longrightarrow \texttt{IsCons(x)}$}
    \end{prooftree}
  \end{minipage}
    }
  }
  \caption{A proof that lists with nonzero length satisfy the \texttt{IsCons} predicate,
      in natural deduction style. Compare with the same proof using the \texttt{Proof} monad
      in listing ****; the steps after the \texttt{(|/)} operator correspond to the leftmost
      deductions in this proof tree. Note a slight difference: the listing proves
      $|x| = 1 + n \vdash \texttt{IsCons}(x)$, while the derivation in this figure
      proves $\vdash |x| = 1 + n \longrightarrow \texttt{IsCons}(x)$.}
\end{figure*}

\begin{lstlisting}[language=Haskell]
nonzero_length_implies_cons
  :: (Length xs == Succ n)
  -> Proof (IsCons xs)

nonzero_length_implies_cons eq =
  do  toSpec length
   |$ or_elimR and_elimL
   |/ and_elimR
   |. symmetric
   |. transitive' eq
   |. (contradicts' $$ zero_not_succ)
   |. absurd

\end{lstlisting}


%% \section{Case Study \#2: A stack-based calculator}

%% In this case study, we investigate how the GDP technique can be used to
%% acheive some of the safety and expressivity features of dependent types,
%% within a system that only supports non-dependent types.

%% To showcase the method, we will develop a library for carrying out computations
%% with a stack-based calculator. The basic state of the calculator will be
%% represented as a stack of \texttt{Double}s, but we will also introduce a
%% phantom parameter: the ghost of the stack's size.

%% \begin{lstlisting}[language=Haskell]
%%   newtype Stack $nu$ = Stack [Double]
%% \end{lstlisting}

%% We also introduce a type constructor \texttt{S} with the intention that
%% if $\nu$ represents a stack of height $n$, then $\texttt{S } \nu$ represents
%% a stack of height $n + 1$. Since \texttt{S} is only supposed to be applied
%% to phantom types, there is no need for any type of the form \texttt{S t} to
%% be inhabited. As a result, we can use an empty data declaration:
%% \begin{lstlisting}[language=Haskell]
%%   data S $nu$    -- empty data declaration, an uninhabitable type
%% \end{lstlisting}
%% The safe stack operations can then be encoded:
%% \begin{lstlisting}[language=Haskell]
%%   pushStack :: Double -> Stack $nu$ -> Stack (S $nu$)
%%   pushStack x (Stack stk) = Stack (x:xs)

%%   popStack :: Stack (S $nu$) -> (Double, Stack $nu$)
%%   popStack (Stack (x:xs)) = (x, Stack xs)
%%   popStack (Stack []) = error "the spirits have been violated"
%% \end{lstlisting}
%% Finally, we should provide a method for generating ghosts:
%% \begin{lstlisting}[language=Haskell]
%%   testStack :: Stack $nu$ -> (forall $mu$. Maybe (Stack (S $mu$)) -> t) -> t
%%   testStack stack action = action $ case stack of
%%       Stack (_:_) -> Just (coerce stack)
%%       _           -> Nothing
%% \end{lstlisting}

%% \subsection{Impredicativity}
%% There is an interesting issue related to impredacative types that can be seen
%% in the encoding of \texttt{testStack}. First, \texttt{testStack} should take a
%% general stack as input, and either reify the fact that there is at least one
%% element, or result in \texttt{Nothing}. So the natural type to expect is
%% \[\texttt{Stack } \nu \to \texttt{Maybe } (\exists \mu.~ \texttt{Stack } (\texttt{S } \mu)).\]
%% But a straightforward encoding as a rank-2 type with universal quantification leads to
%% \[\texttt{Stack } \nu \to \texttt{Maybe } ((\forall \mu.~ \texttt{Stack } (\texttt{S } \mu) \to t) \to t).\]
%% *****
%% Instead, we have to use the weaker encoding
%% \[\texttt{Stack } \nu \to \exists \mu.~ \texttt{Maybe } (\texttt{Stack } (\texttt{S } \mu)),\]
%% corresponding to the rank-2 type
%% \[\texttt{Stack } \nu \to (\forall \mu.~ \texttt{Maybe } (\texttt{Stack } (\texttt{S } \mu)) \to t) \to t.\]

%% \begin{lstlisting}[language=Haskell]
%%   iget :: IxMonadStateT m p p p
%%   iput :: q -> IxMonadStateT m p q ()
%%   imodify :: (p -> q) -> IxMonadStateT m p q ()

%%   return :: a -> IxMonadStateT m p p a
%%   (>>=) :: IxMonadStateT m p q a -> (a -> IxMonadStateT m q r b) -> IxMonadStateT m p r b
%% \end{lstlisting}

%% \begin{lstlisting}[language=Haskell]
%%   type StackOp $nu$ $mu$ t = IxMonadStateT IO (Stack $nu$) (Stack $mu$) t

%%   push :: Double -> StackOp $nu$ (S $nu$) ()
%%   push x = imodify (pushStack x)
  
%%   pop :: StackOp (S $nu$) $nu$ Double
%%   pop = do
%%     stack <- iget
%%     let (top, rest) = popStack stack
%%     iput rest
%%     return top
%% \end{lstlisting}

%% \section{Case Study \#3: Liquid Haskell inside}

%% \section{Case Study \#4: Ghosts of dependent types}

%% \begin{lstlisting}[language=Haskell]
%%   data S $nu$
%% \end{lstlisting}

%% \begin{lstlisting}[language=Haskell]
%%   pf_commutes :: Plus n m -> Plus m n
%%   pf_assocL   :: Plus a (Plus b c) -> Plus (Plus a b) c
%%   pf_assocR   :: Plus (Plus a b) c -> Plus a (Plus b c)
%%   pf_ident    :: Plus n Z -> n
%%   pf_destruct :: n -> Either (n :=: Z) (n :=: S m)
%% \end{lstlisting}

%% \begin{lstlisting}[language=Haskell]
%%   push :: a -> Stack n a -> Stack (S n) a
%%   pop  :: Stack (S n) a -> (a, Stack n a)
%%   test :: Stack n a -> Either (Stack Z) (Stack (S m))
%% \end{lstlisting}

%% \begin{lstlisting}[language=Haskell]
%%   opAdd :: Stack (S (S n)) -> Stack (S n)
%%   opAdd stack = push (x + y) stack''
%%     where
%%       (x, stack')  = pop stack
%%       (y, stack'') = pop stack'
%% \end{lstlisting}


%% \begin{lstlisting}[language=Haskell]
%%   data Column rho
%%   data Row kappa
%%   data Matrix rho kappa
%% \end{lstlisting}

%% \begin{lstlisting}[language=Haskell]
%% class Euclidean v where
%%   (.+.) :: v -> v -> v
%%   (**)  :: Double -> v -> v
%%   zero  :: v
%%   type family Transposed :: *
%%   transpose :: v -> vT


%% instance Euclidean (Col kappa) where
%%   (Col v1) .+. (Col v2) = Col (v1 Vector.(.+.) v2)
%%   zero = Col (Vector.zero)
%%   type Transposed (Col kappa) = Row kappa
%%   transpose = coerce

%% instance Euclidean (Row rho) where
%%   (Row v1) .+. (Row v2) = Row (v1 Vector.(.+.) v2)
%%   zero = Row (Vector.zero)
%%   type Transposed (Row rho) = Col rho
%%   transpose = coerce

%% instance Euclidean (Matrix rho kappa) where
%%   type Transposed (Matrix rho kappa) = Matrix kappa rho
%%   transpose (Matrix m) = Matrix (V.tranpose m)
  
%% transpose :: Matrix rho kappa -> Matrix kappa rho
%% (.+.) :: Matrix rho kappa -> Matrix rho kappa -> Matrix rho kappa
%% (.*.) :: Matrix rho kappa -> Matrix kappa gamma -> Matrix rho gamma
%% (*.) :: Matrix rho kappa -> Column rho -> Column kappa
%% (.*) :: Row kappa -> Matrix rho kappa -> Row rho
%% inner :: Row kappa -> Col kappa -> Double
%% outer :: Col kappa -> Row rho   -> Matrix rho kappa

%% \end{lstlisting}

%% \begin{lstlisting}[language=Haskell]
%% dimRow :: Vector Double -> (forall rho. Row rho -> t) -> t
%% dimCol :: Vector Double -> (forall kappa. Col kappa -> t) -> t
%% dimMat :: Matrix Double -> (forall rho kappa. Mat rho kappa -> t) -> t

%% alignRow :: Row rho -> Row rho' -> Maybe (rho <~> rho')
%% \end{lstlisting}

%% \begin{lstlisting}[language=Haskell]
%% phi :subsetX: phi' = ProperSubset
%%   { pf_subset   :: Vertex phi -> Vertex phi'
%%   , pf_newvtx   :: Vertex phi'
%%   , pf_classify :: Vertex phi' -> Maybe (Vertex phi)
%%   }
%% \end{lstlisting}

%% \begin{lstlisting}[language=Haskell]
%% coerceWith :: (a ~> b) -> (a -> b)

%% coerceToR :: (a <~> b) -> (a -> b)
%% coerceToL :: (a <~> b) -> (b -> a)

%% phi :subsetX: phi' = ProperSubset
%%   { pf_subset   :: Vertex phi ~> Vertex phi'
%%   , pf_newvtx   :: Vertex phi'
%%   , pf_classify :: Vertex phi' -> Maybe (Vertex phi)
%%   }
%% \end{lstlisting}


\end{document}

\end{document}