Sigmaltons

Sigma.hs

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module Sigma where

import Data.Kind (Type)

type family Sing (i :: k) = (o :: Type) | o -> i

---

data Nat = Z | S Nat

data SNat (n :: Nat) where
  SZ ::           SNat  'Z
  SS :: SNat n -> SNat ('S n)

type instance Sing (x :: Nat) = SNat x

---

data Vector (a :: Type) (length :: Nat) where
  VNil :: Vector a 'Z
  (:>) :: x -> Vector x n -> Vector x ('S n)

infixr 4 :>

data Sigma (f :: k -> Type) where
  Sigma :: Sing x -> f x -> Sigma f

test :: [Sigma (Vector Int)]
test
  = [ Sigma         SZ              VNil
    , Sigma (    SS SZ ) (     2 :> VNil)
    , Sigma (SS (SS SZ)) (1 :> 2 :> VNil)
    ]