<p>I can use GADTs, TypeFamilies, DataKinds, and TypeOperators (just for aesthetics) and create what you're after:</p>

<pre><code>data Term0 varb lamb letb where
    Lam :: lamb -&gt; Term0 varb lamb letb -&gt; Term0 varb lamb letb
    Let :: letb -&gt; Term0 varb lamb letb -&gt; Term0 varb lamb letb -&gt; Term0 varb lamb letb
    Var :: varb -&gt; Term0 varb lamb letb
    App :: Term0 varb lamb letb -&gt; Term0 varb lamb letb -&gt; Term0 varb lamb letb

type Term b = Term0 b b b

data Terms = Lets | Lams | Vars

type family  t /// (ty :: Terms) where
    Term0 a b c /// Vars = Term0 Void b c
    Term0 a b c /// Lams = Term0 a Void c
    Term0 a b c /// Lets = Term0 a b Void

Now, I can write functions with more refined types:

unlet :: Term b -&gt; Term b /// Lets
</code></pre>

CC BY-SA 3.0
2016-07-26T15:41:04.943Z
Thanks for your answer. I dislike GHC's `TypeFamilies` purely on principled grounds: it destroys parametricity and free theorems. I'm also not too comfortable with GADTs, because given a GADT `Foo a`, you can have two isomorphic types `Bar` and `Qux`, such that `Foo Bar` and `Foo Qux` aren't isomorphic. That contradicts the mathematical intuition that functions map equals to equals - and, at the type level, isomorphism is the right notion of equality.
isekaijin
CC BY-SA 3.0
2016-07-27T21:08:33.330Z
I understand your qualms, but it allows for specialized generalizations, something that I find quite valuable in practice.
Samuel Schlesinger
CC BY-SA 3.0
2016-07-26T00:51:37.560Z
2016-07-26T18:06:51.040Z
2016-07-26T18:06:51.040Z
Samuel Schlesinger
<p>These kinds of types -- where you define a subtype (basically) by giving a grammar of the acceptable values -- are called <em>datasort refinements</em>. </p>

<ul>
<li><p>They were introduced by Tim Freeman and Frank Pfenning, in their 1991 PLDI paper, <a href="http://dl.acm.org/citation.cfm?id=113468"><em>Refinement Types for ML</em></a>. </p></li>
<li><p>Rowan Davies studied type inference for refinement types in his PhD thesis, <a href="https://www.cs.cmu.edu/~rwh/theses/davies.pdf"><em>Practical Refinement Type Checking</em></a>. He also implemented it as an extension to SML, but I don't know if it is available online.</p></li>
<li><p>Joshua Dunfield studied how to combine datasort refinements with fancier lightweight type dependency in his thesis, <a href="http://www.cs.cmu.edu/~joshuad/papers/thesis/Dunfield07_Type_Refinements_thesis.pdf"><em>A Unified System of Type Refinements</em></a>. He also implemented it in his <em>Stardust</em> language, which is available online:</p>

<p><a href="http://www.mpi-sws.org/~joshua/stardust/">http://www.mpi-sws.org/~joshua/stardust/</a></p></li>
</ul>

CC BY-SA 3.0
2016-07-06T02:32:54.083Z
Rowan Davies' implementation is available here: https://github.com/rowandavies/sml-cidre
Noam Zeilberger
CC BY-SA 3.0
2016-07-05T13:04:52.633Z
2016-07-05T13:04:52.633Z
Neel Krishnaswami
<p>One of the few things that I dislike about Okasaki's book on purely functional data structures is that his code is littered with inexhaustive pattern matching. As an example, I'll give his implementation of real-time queues (refactored to eliminate unnecessary suspensions):</p>

<pre><code>infixr 5 :::

datatype 'a stream = Nil | ::: of 'a * 'a stream lazy

structure RealTimeQueue :&gt; QUEUE =
struct
  (* front stream, rear list, schedule stream *)
  type 'a queue = 'a stream * 'a list * 'a stream

  (* the front stream is one element shorter than the rear list *)
  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)
    | rotate (Nil, y :: nil, zs) = y ::: $zs

  fun exec (xs, ys, _ ::: $zs) = (xs, ys, zs)
    | exec args = let val xs = rotate args in (xs, nil, xs) end

  (* public operations *)
  val empty = (Nil, nil, Nil)
  fun snoc ((xs, ys, zs), y) = exec (xs, y :: ys, zs)
  fun uncons (x ::: $xs, ys, zs) = SOME (x, exec (xs, ys, zs))
    | uncons _ = NONE
end
</code></pre>

<p>As can be seen <code>rotate</code> isn't exhaustive, because it doesn't cover the case where the rear list is empty. Most Standard ML implementations will generate a warning about it. <em>We</em> know that the rear list can't possibly be empty, because <code>rotate</code>'s precondition is that the rear list one element longer than the front stream. But the <em>type checker</em> doesn't know - and it can't possibly know, because this fact is inexpressible in ML's type system.</p>

<p>Right now, my solution to suppress this warning is the following inelegant hack:</p>

<pre><code>  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)
    | rotate (_, ys, zs) = foldl (fn (x, xs) =&gt; x ::: $xs) zs ys
</code></pre>

<p>But what I really want is a type system that can understand that not every triplet is a valid argument to <code>rotate</code>. I'd like the type system to let me define types like:</p>

<pre><code>type 'a triplet = 'a stream * 'a list * 'a stream

subtype 'a queue of 'a triplet
  = (Nil, nil, Nil)
  | (xs, ys, zs) : 'a queue =&gt; (_ ::: $xs, _ :: ys, zs)
  | (xs, ys, zs) : 'a queue =&gt; (_ ::: $xs, ys, _ ::: $zs)
</code></pre>

<p>And then infer:</p>

<pre><code>subtype 'a rotatable of 'a triplet
  = (xs, ys, _) : 'a rotatable =&gt; (_ ::: $xs, _ :: ys, _)
  | (Nil, y :: nil, _)

subtype 'a executable of 'a triplet
  = (xs, ys, zs) : 'a queue =&gt; (xs, ys, _ ::: $zs)
  | (xs, ys, Nil) : 'a rotatable =&gt; (xs, ys, Nil)

val rotate : 'a rotatable -&gt; 'a stream
val exec : 'a executable -&gt; 'a queue
</code></pre>

<p>However, I don't want full-blown dependent types, or even GADTs, or any of the other crazy things certain programmers use. I just want to define subtypes by “carving out” inductively defined subsets of existing ML types. Is this feasible?</p>

<type-theory><type-inference>
Subtypes as subsets of SML datatypes
isekaijin
# Subtypes as subsets of SML datatypes

(Asked by: username_0 on 2016-07-05)

One of the few things that I dislike about Okasaki's book on purely functional data structures is that his code is littered with inexhaustive pattern matching. As an example, I'll give his implementation of real-time queues (refactored to eliminate unnecessary suspensions):
infixr 5 :::

datatype 'a stream = Nil | ::: of 'a * 'a stream lazy

structure RealTimeQueue :> QUEUE =
struct
  (* front stream, rear list, schedule stream *)
  type 'a queue = 'a stream * 'a list * 'a stream

  (* the front stream is one element shorter than the rear list *)
  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)
    | rotate (Nil, y :: nil, zs) = y ::: $zs

  fun exec (xs, ys, _ ::: $zs) = (xs, ys, zs)
    | exec args = let val xs = rotate args in (xs, nil, xs) end

  (* public operations *)
  val empty = (Nil, nil, Nil)
  fun snoc ((xs, ys, zs), y) = exec (xs, y :: ys, zs)
  fun uncons (x ::: $xs, ys, zs) = SOME (x, exec (xs, ys, zs))
    | uncons _ = NONE
end

As can be seen rotate isn't exhaustive, because it doesn't cover the case where the rear list is empty. Most Standard ML implementations will generate a warning about it. We know that the rear list can't possibly be empty, because rotate's precondition is that the rear list one element longer than the front stream. But the type checker doesn't know - and it can't possibly know, because this fact is inexpressible in ML's type system.
Right now, my solution to suppress this warning is the following inelegant hack:
  fun rotate (x ::: $xs, y :: ys, zs) = x ::: $rotate (xs, ys, y ::: $zs)
    | rotate (_, ys, zs) = foldl (fn (x, xs) => x ::: $xs) zs ys

But what I really want is a type system that can understand that not every triplet is a valid argument to rotate. I'd like the type system to let me define types like:
type 'a triplet = 'a stream * 'a list * 'a stream

subtype 'a queue of 'a triplet
  = (Nil, nil, Nil)
  | (xs, ys, zs) : 'a queue => (_ ::: $xs, _ :: ys, zs)
  | (xs, ys, zs) : 'a queue => (_ ::: $xs, ys, _ ::: $zs)

And then infer:
subtype 'a rotatable of 'a triplet
  = (xs, ys, _) : 'a rotatable => (_ ::: $xs, _ :: ys, _)
  | (Nil, y :: nil, _)

subtype 'a executable of 'a triplet
  = (xs, ys, zs) : 'a queue => (xs, ys, _ ::: $zs)
  | (xs, ys, Nil) : 'a rotatable => (xs, ys, Nil)

val rotate : 'a rotatable -> 'a stream
val exec : 'a executable -> 'a queue

However, I don't want full-blown dependent types, or even GADTs, or any of the other crazy things certain programmers use. I just want to define subtypes by “carving out” inductively defined subsets of existing ML types. Is this feasible?

**Tags:** type-theory, type-inference


---

## 2 answers

### Answer by username_2 on 2016-07-05. Score: 21 | Accepted answer

These kinds of types -- where you define a subtype (basically) by giving a grammar of the acceptable values -- are called *datasort refinements*.

* They were introduced by Tim Freeman and Frank Pfenning, in their 1991 PLDI paper, [*Refinement Types for ML*](http://dl.acm.org/citation.cfm?id=113468).
* Rowan Davies studied type inference for refinement types in his PhD thesis, [*Practical Refinement Type Checking*](https://www.cs.cmu.edu/~rwh/theses/davies.pdf). He also implemented it as an extension to SML, but I don't know if it is available online.
* Joshua Dunfield studied how to combine datasort refinements with fancier lightweight type dependency in his thesis, [*A Unified System of Type Refinements*](http://www.cs.cmu.edu/~joshuad/papers/thesis/Dunfield07_Type_Refinements_thesis.pdf). He also implemented it in his *Stardust* language, which is available online:

  <http://www.mpi-sws.org/~joshua/stardust/>

> **Comments:**
> **username_3**: Rowan Davies' implementation is available here: https://github.com/rowandavies/sml-cidre  

---

### Answer by username_1 on 2016-07-26. Score: 1

I can use GADTs, TypeFamilies, DataKinds, and TypeOperators (just for aesthetics) and create what you're after:
data Term0 varb lamb letb where
    Lam :: lamb -> Term0 varb lamb letb -> Term0 varb lamb letb
    Let :: letb -> Term0 varb lamb letb -> Term0 varb lamb letb -> Term0 varb lamb letb
    Var :: varb -> Term0 varb lamb letb
    App :: Term0 varb lamb letb -> Term0 varb lamb letb -> Term0 varb lamb letb

type Term b = Term0 b b b

data Terms = Lets | Lams | Vars

type family  t /// (ty :: Terms) where
    Term0 a b c /// Vars = Term0 Void b c
    Term0 a b c /// Lams = Term0 a Void c
    Term0 a b c /// Lets = Term0 a b Void

Now, I can write functions with more refined types:

unlet :: Term b -> Term b /// Lets

> **Comments:**
> **username_0**: Thanks for your answer. I dislike GHC's `TypeFamilies` purely on principled grounds: it destroys parametricity and free theorems. I'm also not too comfortable with GADTs, because given a GADT `Foo a`, you can have two isomorphic types `Bar` and `Qux`, such that `Foo Bar` and `Foo Qux` aren't isomorphic. That contradicts the mathematical intuition that functions map equals to equals - and, at the type level, isomorphism is the right notion of equality.  
> **username_1**: I understand your qualms, but it allows for specialized generalizations, something that I find quite valuable in practice.  

---

