\documentclass[nocopyrightspace,preprint,blockstyle]{sigplanconf}   % Two-column style

%% \documentclass[draft]{article} 
%% \usepackage{hyperref} 

\usepackage{enumerate}
\usepackage{xspace}
\usepackage{denot}
\usepackage{prooftree}
\usepackage{afterpage}
\usepackage{float}
\usepackage{pstricks}
\usepackage{latexsym} 
%% less space consuming enumerates and itemizes
\usepackage{mdwlist} 
%% \usepackage{stmaryrd} 
\usepackage{amsfonts} 
\usepackage{amssymb} 
%% \usepackage{amsthm} 

% local packages
\usepackage{code}
\usepackage{url} 

\newcommand{\text}[1]{\mbox{#1}}
\usepackage{color} 

\renewcommand{\phi}{\varphi} 

%% \theoremstyle{remark}
%% \newtheorem{example}{Example}[section]
%% \theoremstyle{definition} 
%% \newtheorem{definition}{Definition}[section]
%% \theoremstyle{plain} 
%% \newtheorem{theorem}{Theorem}[section]
%% \newtheorem{lemma}[theorem]{Lemma}
%% \newtheorem{proposition}[theorem]{Proposition}
%% \newtheorem{corollary}[theorem]{Corollary}

\setlength{\parskip}{0.35\baselineskip plus 0.2\baselineskip minus 0.1\baselineskip}
\setlength{\parsep}{\parskip}
\setlength{\topsep}{0cm}
\setlength{\parindent}{0cm}

% Figures should be boxed
%    *** Uncomment the next two lines to box the floats *** 
\floatstyle{boxed}
\restylefloat{figure}
% Keep footnotes on one page
\interfootnotelinepenalty=10000 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Indentation -- attention: works ok for ACM formatting
%% \setlength{\parskip}{0.5\baselineskip plus 0.2\baselineskip minus 0.1\baselineskip}
%% \setlength{\parsep}{\parskip}
%% \setlength{\topsep}{0cm}
%% \setlength{\parindent}{0cm}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{abbrevmap}
\def\rulename#1{\textsc{#1}}
\def\ruleform#1{\fbox{$#1$}}
\def\ol#1{\overline{#1}}
\def\nb{\penalty10000 \ }
\def\fiddle#1{\hspace*{-0.5ex}\raisebox{0.4ex}{$\scriptscriptstyle#1$}}


\newcommand{\trans}[2]{[\![#1]\!]_{#2}} 
% Box around a type
\def\tbox#1{\psframebox[framesep=1pt,linewidth=0.5pt]{#1}}

\newcommand{\highlight}[1]{\colorbox{yellow}{\ensuremath{#1}}}

\newcommand{\as}{\ol{a}}
\newcommand{\bs}{\ol{b}}
\newcommand{\cs}{\ol{c}}
\newcommand{\ds}{\ol{d}}
\newcommand{\es}{\ol{e}}
\newcommand{\fs}{\ol{f}}
\newcommand{\gs}{\ol{g}}
\newcommand{\xs}{\ol{x}}
\newcommand{\alphas}{\ol{\alpha}}
\newcommand{\betas}{\ol{\beta}}
\newcommand{\gammas}{\ol{\gamma}}
\newcommand{\deltas}{\ol{\delta}}
\newcommand{\epsilons}{\ol{\epsilon}}
\newcommand{\zetas}{\ol{\zeta}}
\newcommand{\etas}{\ol{\eta}}

\newcommand{\kappas}{\ol{\kappa}} 
\newcommand{\iotas}{\ol{\iota}} 

\newcommand{\taus}{\ol{\tau}}
\newcommand{\sigmas}{\ol{\sigma}}

%% nasty interaction between denot.sty and abbrev.sty
\def\denot#1{[\![ #1 ]\!]}
\newcommand{\erase}[1]{{\cal E}\denot{#1}}
\newcommand{\typeof}[1]{{\cal T}\denot{#1}}


%% Typing relations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\usepackage{xspace} 
\usepackage{natbib}
\bibpunct();A{},
\let\cite=\citep

\renewcommand{\topfraction}{0.95}
\renewcommand{\textfraction}{0.02}
\renewcommand{\floatpagefraction}{0.8}


\newcommand{\authornote}[3]{\marginpar{\sc\color{#2} #1}\textbf{\textcolor{#2}{#3}}}
\newcommand\simon[1]{\authornote{simon}{red}{#1}}
\newcommand\dv[1]{\authornote{dv}{green}{#1}}
\newcommand\conor[1]{\authronote{conor}{blue}{#1}}

\newcommand{\cokind}{\textsc{co}}      % Kind of coercions
\newcommand{\tykind}{\textsc{ty}}      % Kind of types
\newcommand{\kikind}{\textsc{knd}}

\newcommand{\turnst}{\mathrel{\vdash_{\hspace{-3pt}\tiny \tykind}}}
\newcommand{\turnsc}[1]{\mathrel{\vdash_{\hspace{-3pt}\tiny \cokind}^{\hspace{-2pt}\tiny #1}}}
\newcommand{\turnsk}{\mathrel{\vdash_{\hspace{-3pt}\tiny \kikind}}}


\newcommand{\at}{@} 

\newcommand{\qt}[1]{\text{``}#1\text{''}} 
\newcommand{\lift}[1]{\{#1\}} 

\authorinfo{}{}{}
\usepackage{abbrev}
\begin{document} 

\title{Dependent kinds for Haskell}
\subtitle{\color{red}\today}

\maketitle
\makeatactive 


\begin{abstract}
We explore the addition of a dependent kind (and type) system in Haskell.
 \end{abstract}

\section{Syntax} 

\begin{figure}
\[\begin{array}{l}
   \begin{array}{lcll} 
   \multicolumn{4}{l}{\textbf{Kinds}} \\ 
      \kappa,\iota  & ::= & \star \mid \kappa_1 \Rightarrow \kappa_2 \mid \lift{\tau} \mid \forall(a{:}\kappa_1).\kappa_2  &  \\ \\ 
   \multicolumn{4}{l}{\textbf{Types}} \\ 
      \tau    & ::= & a \mid @T@ \mid F_n\;\taus^n \mid \tau_1 \to \tau_2 \mid \forall(a{:}\kappa).\tau \\ 
           & \mid   & \tau_1\at{\tau_2} \mid \lift{C} \mid \qt{\kappa} \mid \lift{x}
   \end{array}
\end{array}\]
\caption{Syntax}\label{fig:syntax}
\end{figure}

Our first goal is to add a proper kind system with kinds that depend on types. In 
Figure~\ref{fig:syntax}, the form $\lift{\tau}$ achieves exactly that. For example, we 
may declare a {\em datatype}: 
\begin{code} 
  data Nat : * where 
    Z :: Nat 
    S :: Nat -> Nat
\end{code} 
which immediately gives rise to a {\em datakind}, $\lift{@Nat@}$, a lifted
version of @Nat@ to the level of kinds (or a singleton kind), inhabited by the 
type @Nat@. Hence, Figure~\ref{fig:syntax} allows such kinds, of the form 
$\lift{\tau}$. Figure~\ref{fig:wf-kinds} gives the well-formedness relation on kinds. 

\begin{figure}
\[\begin{array}{c}
\ruleform{ \Gamma \turnsk \kappa } \\ \\  
\prooftree
  ----------------{kstar}
  \Gamma \turnsk \star 
  ~~~~ 
  \Gamma \turnsk \kappa_1 \quad \Gamma \turnsk \kappa_2
  ----------------------{karr} 
  \Gamma \turnsk \kappa_1 \Rightarrow \kappa_2
  ~~~~~ 
  \Gamma \turnst \tau : \star 
  ----------------------------{klift}
  \Gamma \turnsk \lift{\tau}
  ~~~~ 
  \Gamma,(a{:}\kappa_1) \turnsk \kappa_2 \quad \Gamma \turnsk \kappa_1
  -------------------------------{kall} 
   \Gamma \turnsk \forall(a{:}\kappa_1).\kappa_2 
\endprooftree
\end{array}\]  
\caption{Well-formed kinds}\label{fig:wf-kinds}
\end{figure}

Notice that the judgement $\Gamma \turnsk \kappa$ relies on the well-formedness relation 
on types $\Gamma \turnst \tau : \kappa$, to be discussed next.  

The next question is what happens at the type level. Let us consider the case of data constructors. 
Since @Nat@ can be lifted to the kind $\lift{@Nat@}$ we would expect that each of the constructors
could be lifted to {\em types}. For example @Z@ could be lifted to form the type 
$\lift{@Z@}$, of kind $\lift{@Nat@}$. 

However, for @S@ the situation is more complex. For @S@, of type 
$@Nat@ \to @Nat@$, we have (at least) two options for giving a kind to 
the lifted constructor @S@: 
\begin{itemize}
  \item Give $\lift{@S@}$ the kind $\lift{@Nat@ \to @Nat@}$, or 
  \item Give $\lift{@S@}$ the kind $\lift{@Nat@} \Rightarrow \lift{@Nat@}$.  
\end{itemize}
In other words, should we be ``pushing'' the lift operator under $\to$, translating 
it to $\Rightarrow$ or not? It certainly is more expressive to allow the pushing but maybe
the complexity is not worth it.

Concretely, we have examined the following options: 
\begin{enumerate} 
  \item Do no pushing of the ``lift'' operation on types at all. But, in order to 
        maintain some reasonable expressivity we will instead extend the syntax of 
        liftable expressions from data constructors and variables ($C$ and $x$ respectively
        in Figure~\ref{fig:syntax} to a bigger set of expressions consisting of applications
        of data constructors and variables $c$, below: 
        \[\begin{array}{lcl} 
            c & ::= & C \mid x \mid c\;c \mid c\;[\tau] \mid a 
        \end{array}\] 
        We include type variables $a$ in that set of expression if they are of kind $\lift{\tau}$. 
        \dv{we need an example here}
        Hence, the type $\lift{@S@}\;\lift{@Z@}$ is not well-formed, but this application
        can be recovered by the expression $\lift{@S Z@}$. Hence the typing relation for that 
        limited set of expressions would be: 
        \[\begin{array}{c}\prooftree
            \Gamma \vdash_c c : \tau 
           --------------{ty}
            \Gamma \turnst \lift{c} : \lift{\tau} 
           ~~~~ 
            (a{:}\lift{\tau}) \in \Gamma
           --------------------{var}
            \Gamma \vdash_c a : \tau 
           ~~~~~ 
            (C{:}\tau) \in \Gamma 
           ---------------------{con} 
            \Gamma \vdash_c C : \tau 
           ~~~~  
           \Gamma \vdash_c c_1 : \tau_1 \to \tau_2 \quad \Gamma \vdash_c c_2 :\tau_1
           ------------------------{tapp}
           \Gamma \vdash_c c_1\;c_2 : \tau_2
           ~~~~~ 
           \Gamma \vdash_c c : \forall(a{:}\kappa_1).\kappa_2 \quad \Gamma \vdash_c \tau : \kappa_1
           ------------------------{tapp}
           \Gamma \vdash_c c\;[\tau] : \kappa_2\{\tau/a\}    
        \endprooftree\end{array}\]
        One problem with this approach is that lifting for variables that abstract singleton
        kinds seems redundant. For example we have: 
        \[  (a{:}\lift{\tau}) \turnst a : \lift{\tau}  \] 
        but we also have: 
        \[  (a{:}\lift{\tau}) \turnst \lift{a} : \lift{\tau}  \] 
        A question arises: do we consider $\lift{a}$ and $a$ equivalent, or not? 
        If yes, this approach does not have the simplicity that we were initally attracted by; if 
        not, then programs may fail unexpectedly (e.g. if a function expects a $\lift{a}$ and one 
        passes it a $a$ argument). 
  \item Allowing lifting over arrows, as a function $lift$ which is partially evaluated -- evaluation
        stops when you reach an abstract type variabe. Hence, the rule would be: 
        \[\begin{array}{c}\prooftree
           (C{:}\tau) \in \Gamma \quad lift(\tau) ~~> \kappa 
           ------------------------{liftcon}
           \Gamma \vdash \lift{C} : \kappa 
        \endprooftree\end{array}\]
        One problem with this approach is that the resulting system is not stable under substitutions. If 
        a function $f$ has type $a \to @Nat@ \to a$ then lifting its type would give 
        $\lift{a} \Rightarrow \lift{@Nat@} \Rightarrow \lift{a}$. However when $a$ was going to be substituted away for, e.g.
        $@Nat@ \to @Nat@$ then we would not be able to expose the kind 
        \[(\lift{@Nat@} \Rightarrow \lift{@Nat@}) \Rightarrow \lift{@Nat@} \Rightarrow \lift{@Nat@} \Rightarrow \lift{@Nat@} \] 
        for it. Hence, we arrive at the third option, which is: 
  \item Allow lifting over arrows via a partially evaluated function {\em and} make substitution 
        push the lifting braces down the structure of the type. Both could be achieved with a single function $push$ 
        that pushes the braces in the types down arrows, as much as possible. 
        For example, the rule for eliminating types with polymorphic kinds would be: 
        \[\begin{array}{c}\prooftree
           \Gamma \turnst \tau_1 : \forall(a{:}\kappa_1).\kappa_2 \quad \Gamma \turnst \tau_2 : \kappa_1
           --------------------------------------------------{eall}
           \Gamma \turnst \tau_1\at{\tau_2} : push(\kappa_2\{\tau_2/a\})
        \endprooftree\end{array}\]
        The rule for lifting a constructor would be: 
        \[\begin{array}{c}\prooftree
           (C{:}\sigma) \in \Gamma 
           ----------------------------------------------{lcon}
           \Gamma \turnst \lift{C} : push(\lift{\sigma})
        \endprooftree\end{array}\]
        \dv{This is very reminiscent of the ``boxy substitution'' formalization we used in the FPH paper. But there 
            the pushing was formed as a subsumption rule not as a function eagerly applied} 
\end{enumerate} 

\section{Lifting types, lowering kinds} 

Suppose that we wish to write the following version of the equality GADT:
\begin{code}
  data Eq :: forall a b. {a} => {b} => * where 
    Refl :: forall (a:*) (b:{a}). Eq b b 
\end{code} 
The kind of @Eq@ says that it may accept a value of a datakind and another 
datakind and will ensure that the two are the same. This can be used to encode
term-level equalities: 
\begin{code}
  Refl @ Nat @ {Z} : Eq {Z} {Z}  
\end{code} 
But we may wish to use it to encode {\em type-level} equalities as well! We
would like to say something like: 
\begin{code} 
  Refl@ ?a @ Nat : Eq Nat Nat  
\end{code} 
But now the problem is {\em what do we plug in for} the instantatiation @?a@? 
Intuitively we need something such that @Nat : {?a}@ and hence it would have 
to be an operator on kinds that cancels-out with lifting. We introduce that operator
and we call it quote: 
\[\begin{array}{c}\prooftree
       \Gamma \turnsk \kappa 
    -------------------------{qt}
    \Gamma \turnst \qt{\kappa} : \star 
\endprooftree\end{array}\]
with the equality that: 
\[        \lift{\qt{\kappa}} \equiv \kappa \] 
In effect we created an uninhabited type, which is just a name for a particular kind. 
We may now write:
\begin{code} 
  Refl@ ``*'' @ Nat : Eq Nat Nat
  Refl@ ``*->*'' @ Maybe : Eq Maybe Maybe  
\end{code} 

Such quoted kinds can be generally useful for representing 
heterogeneous data structures. In Figure~\ref{fig:hrec} we give a more 
substantial example of such a data structure. 

\begin{figure*}[ht] 
\begin{code}
  data Rec ::  {[(String,``*'')]} => * where 
    RNil  :: Rec {[]} 
    RCons :: forall (a :: *) 
                    (ns :: {[(String,``*'')]} 
                    (s :: String). a -> Rec ns -> Rec { ({:}@(String,``*'')) ({()} s a) ns }
                                   -- just Rec {(s,a):ns} really, but well-typed
\end{code} 
\caption{Heterogeneous records with fixed labels}\label{fig:hrec} 
\end{figure*}

The example in Figure~\ref{fig:hrec} also demonstrates that we probably need better syntax, or syntactic
sugar, or some form of type abbreviations. 


\clearpage
\section{Type inference and unification} 

We do not expect any serious problems here --- we simply have to be careful that we
decompose the typing equality problems enough so that we do not forget about the constraints arising
from the corresponding kind equality problems. 






%% \makebibliography{./local-bib-one,./local-bib-two}
\end{document}