1
$\begingroup$

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:

  1. From the POV of language implementors, can this restriction simplify type checking? How much?

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

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

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Kaveh Jun 16 '16 at 2:01
  • $\begingroup$ @Kaveh: Okay, rewritten. $\endgroup$ – pyon Jun 16 '16 at 2:32
  • 1
    $\begingroup$ 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. $\endgroup$ – Stefan Jun 16 '16 at 4:36
  • $\begingroup$ @Stefan: Good point! Then my restriction isn't thorough enough. I'll think about it more carefully before re-editing my question. $\endgroup$ – pyon Jun 16 '16 at 4:45
  • 1
    $\begingroup$ 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? $\endgroup$ – Andrej Bauer Jun 16 '16 at 15:55
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – pyon Jun 16 '16 at 16:59
  • 1
    $\begingroup$ No, you need both $\prod$-types and inductive typed (data) to get identity types. $\endgroup$ – Andrej Bauer Jun 17 '16 at 10:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.