84 lines
1.9 KiB
Haskell
84 lines
1.9 KiB
Haskell
{-# LANGUAGE DataKinds #-}
|
|
{-# LANGUAGE GADTs #-}
|
|
{-# LANGUAGE TypeOperators #-}
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
|
|
-- https://blog.jle.im/entry/fixed-length-vector-types-in-haskell-2015.html
|
|
|
|
module Types where
|
|
|
|
-- Nat is a type of a set of types here (thanks to DataKinds extension
|
|
-- ie, constructors of `Nat' are types. Not values
|
|
-- :k
|
|
data Nat
|
|
= Z
|
|
| S Nat
|
|
--deriving Show
|
|
-- ghci> :k Nat
|
|
-- Nat :: *
|
|
-- ghci> :k Z
|
|
-- Z :: Nat
|
|
-- ghci> :k S
|
|
-- S :: Nat -> Nat
|
|
-- ghci> :k 'S
|
|
-- 'S :: Nat -> Nat
|
|
|
|
|
|
data Vec :: Nat -> * -> * where
|
|
Nil :: Vec 'Z a
|
|
(:>) :: a -> Vec n a -> Vec ('S n) a
|
|
|
|
infixr 5 :>
|
|
deriving instance Show a => Show (Vec n a)
|
|
deriving instance Eq a => Eq (Vec n a)
|
|
|
|
hd :: Vec ('S n) a -> a
|
|
hd (x :> _) = x
|
|
|
|
-- λ> hd (1 :> 2 :> Nil)
|
|
-- 1
|
|
-- λ> hd (Nil)
|
|
-- * Couldn't match type 'Z with 'S n0
|
|
-- Expected: Vec ('S n0) a
|
|
-- Actual: Vec 'Z a
|
|
-- * In the first argument of `hd', namely `(Nil)'
|
|
-- In the expression: hd (Nil)
|
|
-- In an equation for `it': it = hd (Nil)
|
|
|
|
|
|
tl :: Vec ('S n) a -> Vec n a
|
|
tl (_ :> xs) = xs
|
|
|
|
-- tl (1 :> 2 :> Nil) :: Num a => Vec ('S 'Z) a
|
|
-- λ> :t tl
|
|
-- tl :: Vec ('S n) a -> Vec n a
|
|
-- λ> tl (1 :> Nil)
|
|
-- tl (1 :> Nil) :: Num a => Vec 'Z a
|
|
|
|
|
|
-- https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_families.html#extension-TypeFamilies
|
|
|
|
-- Addition at type level
|
|
type family (+) (x :: Nat) (y :: Nat) where
|
|
'Z + y = y
|
|
--x + 'Z = x -- not in blog post
|
|
('S x) + y = 'S (x + y)
|
|
|
|
-- Addition for values of the `Nat' type
|
|
(+>) :: Nat -> Nat -> Nat
|
|
Z +> y = y
|
|
(S x) +> (S y) = S (x +> y)
|
|
|
|
append :: Vec n a -> Vec m a -> Vec (n + m) a
|
|
append (x :> v1') v2 = x :> (append v1' v2)
|
|
append Nil v2 = v2
|
|
--append v1 Nil = v1 -- not in blog post
|
|
|
|
-- λ> append (1 :> 2 :> Nil) (3 :> 4 :> 5 :> Nil)
|
|
-- append (1 :> 2 :> Nil) (3 :> 4 :> 5 :> Nil)
|
|
-- :: Num a => Vec ('S ('S ('S ('S ('S 'Z))))) a
|
|
|
|
-- --After giving Show
|
|
-- λ> append (1 :> 2 :> Nil) (3 :> 4 :> 5 :> Nil)
|
|
-- 1 :> (2 :> (3 :> (4 :> (5 :> Nil))))
|