tuples.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
module Test where

import GHC.TypeLits

newtype Single a = Single a

type family TupleTypes (tuple :: *) :: [*] where
  TupleTypes () = '[]
  TupleTypes (Single a) = '[a]
  TupleTypes (a, b) = '[a, b]
  TupleTypes (a, b, c) = '[a, b, c]

type family Length (tys :: [k]) :: Nat where
  Length '[] = 0
  Length (a ': as) = 1 + Length as

data V (len :: Nat) = V

type family AllDoubles_ (tys :: [*]) :: * where
  AllDoubles_ '[] = ()
  AllDoubles_ (Double ': as) = AllDoubles_ as
type AllDoubles as = AllDoubles_ as ~ ()

vToTuple :: (types ~ TupleTypes tuple, Length types ~ len, AllDoubles types) => V len -> tuple
vToTuple = error "TODO"

vFromTuple :: (types ~ TupleTypes tuple, Length types ~ len, AllDoubles types) => tuple -> V len
vFromTuple = error "TODO"

{-
*Test> :t vToTuple (V @3)
vToTuple (V @3)
  :: (AllDoubles_ (TupleTypes tuple) ~ (),
      Length (TupleTypes tuple) ~ 3) =>
     tuple
*Test> :t vToTuple (V @3) :: (Double, Double, Double)
vToTuple (V @3) :: (Double, Double, Double)
  :: (Double, Double, Double)
-}