<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.  

---

