Skip to content

Instantly share code, notes, and snippets.

@cdparks

cdparks/Vector.hs

Last active Jan 26, 2018
Embed
What would you like to do?
Convert type-level lists to term-level sized-vectors
#!/usr/bin/env stack
-- stack --resolver lts-10.3 script --package ghc-typelits-natnormalise
{-
$ tail -2 Vector.hs
print $ toVector @[1, 2, 3, 4, 5]
print $ toVector @["whomp", "merp", "yarp"]
$ ./Vector.hs
Cons 1 (Cons 2 (Cons 3 (Cons 4 (Cons 5 Nil))))
Cons "whomp" (Cons "merp" (Cons "yarp" Nil))
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
import Data.Kind
import Data.Proxy
import GHC.TypeLits
data Vector :: Nat -> Type -> Type where
Nil :: Vector 0 a
Cons :: a -> Vector n a -> Vector (n + 1) a
deriving instance Show a => Show (Vector n a)
type family Length (xs :: [k]) where
Length '[] = 0
Length (_ ': xs) = 1 + Length xs
class ToTerm (k :: Type) (t :: k) (e :: Type) | k -> e, t -> e where
toTerm :: proxy t -> e
instance KnownSymbol s => ToTerm Symbol s String where
toTerm = symbolVal
instance KnownNat n => ToTerm Nat n Integer where
toTerm = natVal
class ToVector ts e where
toVector :: Vector (Length ts) e
instance ToVector '[] e where
toVector = Nil
instance (ToTerm k t e, ToVector ts e) => ToVector (t ': ts) e where
toVector = Cons (toTerm (Proxy @t)) (toVector @ts)
main :: IO ()
main = do
print $ toVector @[1, 2, 3, 4, 5]
print $ toVector @["whomp", "merp", "yarp"]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.