<p><strong>This is not a real restriction to the power of the language</strong></p>

<p>First, it is possible to turn all indices of the type family into variables by adding extra arguments to the constructor expressing the constraints. For example, <code>Test</code> can be turned into</p>

<p><code>data Test a where
  Foo :: Integer -&gt; a = Color -&gt; Test a
  Bar :: Float   -&gt; a = Sign -&gt; Test a
</code></p>

<p>Second, you can define your own version of the propositional equality as an inductive family and use that instead of the built-in one.</p>

<p><code>data Eq :: * -&gt; * -&gt; * where
  Refl :: Eq a a
</code></p>

<p>This definition follows your restrictions, but it won't be detected as being 'the' identity type. (In case you want to build in some kind of detection for identity-like types, I'd guess that the property of being identity-like may well be undecidable.) So there is nothing that you can do without your restriction that you couldn't do with it in a (somewhat) more complicated way. </p>

CC BY-SA 3.0
2016-06-16T16:59:01.220Z
So, basically, if you have $\Pi$-types, identity types are “already there”, and it doesn't make sense to constrain how identity types can be used without constraining how $\Pi$-types can be used?
isekaijin
CC BY-SA 3.0
2016-06-17T10:13:50.980Z
No, you need both $\prod$-types *and* inductive typed (`data`) to get identity types.
Andrej Bauer
CC BY-SA 3.0
2016-06-16T10:14:27.253Z
2016-06-16T10:14:27.253Z
Jesper
<p>Let a simple expression be either:</p>

<ul>
<li>A free variable</li>
<li>A data constructor of an <em>inductive</em> type family, applied to 0 or more simple expressions</li>
</ul>

<p>What would be the effect of imposing the following restriction on a programming language with inductive type families?</p>

<blockquote>
  <p>Given a data constructor <code>C</code> of an inductive type family <code>T</code>, within <code>C</code>'s type signature, <code>T</code> and <code>(=)</code> (the propositional equality type constructor) may only appear <em>fully</em> applied to simple expressions whose free variables are bound within the type signature itself.</p>
</blockquote>

<p>For example, in GHC Haskell (to avoid writing <code>forall</code>s in obvious places):</p>

<pre><code>{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Color = Red | Black
data Sign = Positive | Negative

-- Bad: Test appears applied to Color and Sign, neither
-- of which is a data constructor of an inductive type.
data Test :: * -&gt; * where
  Foo :: Integer -&gt; Test Color
  Bar :: Float   -&gt; Test Sign

-- Good: List only appears applied to free variables.
data List :: (k -&gt; k -&gt; *) -&gt; k -&gt; k -&gt; * where
  Nil  ::                        List f a a
  Cons :: f a b -&gt; List f b c -&gt; List f a c

-- Good: RBT appears applied to Black and Red, both of
-- which are constructors of an inductive type (Color).
data RBT :: Color -&gt; * -&gt; * where
  Empty ::                                    RBT Black a
  R     :: RBT Black a -&gt; a -&gt; RBT Black a -&gt; RBT Red   a
  B     :: RBT l     a -&gt; a -&gt; RBT r     a -&gt; RBT Black a
</code></pre>

<p>Now, what I want to know is:</p>

<ol>
<li><p>From the POV of language implementors, can this restriction simplify type checking? How much?</p></li>
<li><p>From the POV of programmers using languages like Agda, Idris, Coq, etc., are there any useful programs that type check without the restriction, that can't be refactored into equivalent programs that type check under the restriction?</p></li>
<li><p>From the POV of type theorists and other mathematicians using type theory as a foundational system, does the restriction prevent any useful mathematical results from being obtained internally to type theory?</p></li>
</ol>

CC BY-SA 3.0
2016-06-16T02:01:31.777Z
The question is hard to understand. Please edit your question to be concise, clear, and to the point. Also you should try to be more precise by what you mean by "this", a pair of positive and negative examples is not enough to define what you have in mind.
Kaveh
CC BY-SA 3.0
2016-06-16T02:32:45.270Z
@Kaveh: Okay, rewritten.
isekaijin
CC BY-SA 3.0
2016-06-16T04:36:42.403Z
I still have trouble understanding the "avoid needing to explicitly use the univalence axiom" and the restriction you're trying to impose.  To give you a concrete example: if you change `Foo` to be `Foo :: ∀a. Integer -> (a = Color) -> Test a`, it looks to me like your restriction is obeyed, yet you're back with the same problem.
Stefan
CC BY-SA 3.0
2016-06-16T04:45:21.583Z
@Stefan: Good point! Then my restriction isn't thorough enough. I'll think about it more carefully before re-editing my question.
isekaijin
CC BY-SA 3.0
2016-06-16T05:22:03.930Z
@Stefan: Edited. The new version of my restriction now also forbids your version of `Foo`.
isekaijin
CC BY-SA 3.0
2016-06-16T05:36:48.967Z
@Stefan: My beef with UA (and axioms in general) is that I think of axioms as restrictions on model construction, so my only way to make sense of axioms is by looking at models where they hold. OTOH, I can make sense of natural deduction rules by looking at how intro/elim pairs drive computations. Not having to look at models of type theory is a good thing for me, because models of type theory look like big, scary things.
isekaijin
CC BY-SA 3.0
2016-06-16T15:55:06.017Z
The question is still unclear. What is this talk of univalence axiom? Please make it precise. Or to put it another way: can you pick *either* type theoretic terminology *or* Haskell, but not mix both arbitrarily?
Andrej Bauer
<type-theory><dependent-type>
What's the effect of imposing the following restriction on inductive type families?
isekaijin
# What's the effect of imposing the following restriction on inductive type families?

(Asked by: username_0 on 2016-06-15)

Let a simple expression be either:

A free variable
A data constructor of an inductive type family, applied to 0 or more simple expressions

What would be the effect of imposing the following restriction on a programming language with inductive type families?

Given a data constructor C of an inductive type family T, within C's type signature, T and (=) (the propositional equality type constructor) may only appear fully applied to simple expressions whose free variables are bound within the type signature itself.

For example, in GHC Haskell (to avoid writing foralls in obvious places):
{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Color = Red | Black
data Sign = Positive | Negative

-- Bad: Test appears applied to Color and Sign, neither
-- of which is a data constructor of an inductive type.
data Test :: * -> * where
  Foo :: Integer -> Test Color
  Bar :: Float   -> Test Sign

-- Good: List only appears applied to free variables.
data List :: (k -> k -> *) -> k -> k -> * where
  Nil  ::                        List f a a
  Cons :: f a b -> List f b c -> List f a c

-- Good: RBT appears applied to Black and Red, both of
-- which are constructors of an inductive type (Color).
data RBT :: Color -> * -> * where
  Empty ::                                    RBT Black a
  R     :: RBT Black a -> a -> RBT Black a -> RBT Red   a
  B     :: RBT l     a -> a -> RBT r     a -> RBT Black a

Now, what I want to know is:

From the POV of language implementors, can this restriction simplify type checking? How much?
From the POV of programmers using languages like Agda, Idris, Coq, etc., are there any useful programs that type check without the restriction, that can't be refactored into equivalent programs that type check under the restriction?
From the POV of type theorists and other mathematicians using type theory as a foundational system, does the restriction prevent any useful mathematical results from being obtained internally to type theory?

**Tags:** type-theory, dependent-type

> **Comments:**
> **username_1**: The question is hard to understand. Please edit your question to be concise, clear, and to the point. Also you should try to be more precise by what you mean by "this", a pair of positive and negative examples is not enough to define what you have in mind.  
> **username_0**: @username_1: Okay, rewritten.  
> **username_2**: I still have trouble understanding the "avoid needing to explicitly use the univalence axiom" and the restriction you're trying to impose.  To give you a concrete example: if you change `Foo` to be `Foo :: ∀a. Integer -> (a = Color) -> Test a`, it looks to me like your restriction is obeyed, yet you're back with the same problem.  
> **username_0**: @username_2: Good point! Then my restriction isn't thorough enough. I'll think about it more carefully before re-editing my question.  
> **username_0**: @username_2: Edited. The new version of my restriction now also forbids your version of `Foo`.  
> **username_0**: @username_2: My beef with UA (and axioms in general) is that I think of axioms as restrictions on model construction, so my only way to make sense of axioms is by looking at models where they hold. OTOH, I can make sense of natural deduction rules by looking at how intro/elim pairs drive computations. Not having to look at models of type theory is a good thing for me, because models of type theory look like big, scary things.  
> **username_3**: The question is still unclear. What is this talk of univalence axiom? Please make it precise. Or to put it another way: can you pick *either* type theoretic terminology *or* Haskell, but not mix both arbitrarily?  

---

## 1 answers

### Answer by username_4 on 2016-06-16. Score: 5 | Accepted answer

**This is not a real restriction to the power of the language**

First, it is possible to turn all indices of the type family into variables by adding extra arguments to the constructor expressing the constraints. For example, `Test` can be turned into

`data Test a where
Foo :: Integer -> a = Color -> Test a
Bar :: Float -> a = Sign -> Test a`

Second, you can define your own version of the propositional equality as an inductive family and use that instead of the built-in one.

`data Eq :: * -> * -> * where
Refl :: Eq a a`

This definition follows your restrictions, but it won't be detected as being 'the' identity type. (In case you want to build in some kind of detection for identity-like types, I'd guess that the property of being identity-like may well be undecidable.) So there is nothing that you can do without your restriction that you couldn't do with it in a (somewhat) more complicated way.

> **Comments:**
> **username_0**: So, basically, if you have $\Pi$-types, identity types are “already there”, and it doesn't make sense to constrain how identity types can be used without constraining how $\Pi$-types can be used?  
> **username_3**: No, you need both $\prod$-types *and* inductive typed (`data`) to get identity types.  

---

