haskelltuplesdata-kinds

Can I teach GHC mathematical induction?

I attempted to create a datatype representing a tuple of infinitely many types:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeNats

infixr 5 :!!

data OmegaTuple (t :: Nat -> *) (n :: Nat) = t n :!! OmegaTuple t (n+1)

This is fine.

I also attempted to declare the direct product of infinitely many semigroups:

instance (Semigroup (t n), Semigroup (OmegaTuple t (n+1))) => Semigroup (OmegaTuple t n) where
    (x :!! xs) <> (y :!! ys) = x <> y :!! xs <> ys

Yet GHC complains like this:

• Illegal nested constraint ‘Semigroup (OmegaTuple t (n + 1))’
  (Use UndecidableInstances to permit this)

If I understood correctly, using UndecidableInstances will make GHC fall in an infinite loop.

Another attempt:

instance (Semigroup (t n), forall k. Semigroup (t k) => Semigroup (t (k+1))) => Semigroup (OmegaTuple t n) where
    (x :!! xs) <> (y :!! ys) = x <> y :!! xs <> ys

Then GHC complains like this:

• Illegal type synonym family application ‘k + 1’ in instance:
    Semigroup (t (k + 1))

Is it really impossible to teach GHC mathematical induction?

Solution

  • You can manually wrap the dictionaries, that allows lazily building up an “infinite class dictionary”:

    {-# LANGUAGE GADTs     #-}
{-# LANGUAGE DataKinds #-}
 
import Data.Kind (Type)
import GHC.TypeLits

data SemigroupSequence (t :: Nat -> Type) (n :: Nat) where
  SemigroupSequence :: Semigroup (t n)
     => SemigroupSequence t (n+1) -> SemigroupSequence t n

class SemigroupFamily t where
  semigroupSequence :: SemigroupSequence t 0

    and then

    mappendOmega :: SemigroupSequence t n
     -> OmegaTuple t n -> OmegaTuple t n -> OmegaTuple t n
mappendOmega (SemigroupSequence sd') (x :!! xs) (y :!! ys)
   = x <> y :!! mappendOmega sd' xs ys

instance (SemigroupFamily t) => Semigroup (OmegaTuple t 0) where
  (<>) = mappendOmega semigroupSequence