Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Proofs involving conversion from and to length-indexed vectors
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module FromToVec where
import Data.Kind
import Data.Type.Equality
type Sing :: k -> Type
type family Sing
type SList :: [a] -> Type
data SList l where
SNil :: SList '[]
(:%) :: Sing x -> SList xs -> SList (x : xs)
type instance Sing @[a] = SList
type Nat :: Type
data Nat where
Z :: Nat
S :: Nat -> Nat
type Vec :: Type -> Nat -> Type
data Vec a n where
VNil :: Vec a Z
(:>) :: a -> Vec a n -> Vec a (S n)
type SVec :: Vec a n -> Type
data SVec v where
SVNil :: SVec VNil
(:%>) :: Sing x -> SVec xs -> SVec (x :> xs)
type instance Sing @(Vec a n) = SVec
type FromVec :: Vec a n -> [a]
type family FromVec v where
FromVec VNil = '[]
FromVec (x :> xs) = x : FromVec xs
type Len :: [a] -> Nat
type family Len l where
Len '[] = Z
Len (_ : xs) = S (Len xs)
type ToVec :: forall a. forall (l :: [a]) -> Vec a (Len l)
type family ToVec l where
ToVec '[] = VNil
ToVec (x : xs) = x :> ToVec xs
fromToVec :: forall a (l :: [a]).
SList l -> FromVec (ToVec l) :~: l
fromToVec SNil = Refl
fromToVec (_ :% sxs)
| Refl <- fromToVec sxs
= Refl
toFromVec :: forall a n (v :: Vec a n).
SVec v -> ToVec (FromVec v) :~~: v
toFromVec SVNil = HRefl
toFromVec (_ :%> sxs)
| HRefl <- toFromVec sxs
= HRefl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment