tuples.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}

module Tuple where

import Data.Kind
  ( Type )

data Nat :: Type where
  Zero :: Nat
  Succ :: Nat -> Nat

data SNat :: Nat -> Type where
  SZero :: SNat Zero
  SSucc :: SingI n => SNat (Succ n)

class SingI (n :: Nat) where
  sing :: SNat n

instance SingI Zero where
  sing = SZero

instance SingI n => SingI (Succ n) where
  sing = SSucc @n

data Fin :: Nat -> Type where
  FZero :: Fin (Succ n)
  FSucc :: !(Fin n) -> Fin (Succ n)

type Tuple (n :: Nat) (a :: Type) = Fin n -> a

universe :: forall n. SingI n => [Fin n]
universe = case sing @n of
  SZero -> []
  ss@(SSucc :: SNat n) ->
    case ss of
      ( _ :: SNat (Succ m) ) ->
        FZero : map FSucc universe

toList :: SingI n => Tuple n a -> [a]
toList tup = map tup universe