From 5685da9e7a43f35827b9071e69dc340ee2e82bb7 Mon Sep 17 00:00:00 2001
From: Julin S <famubu@rawtext.club>
Date: Mon, 25 Sep 2023 22:43:06 +0530
Subject: [PATCH] [haskell] Try some ghc extensions

---
 haskell/README.org |  2 ++
 haskell/types.hs   | 83 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 85 insertions(+)
 create mode 100644 haskell/types.hs

diff --git a/haskell/README.org b/haskell/README.org
index 162216a..cfd3cff 100644
--- a/haskell/README.org
+++ b/haskell/README.org
@@ -1,3 +1,5 @@
 #+TITLE: Haskell
 
  - [[./state-monad.hs][state-monad.hs]]: Demo of state monad using postfix expression evaluator
+ - [[./types.hs]]: Trying out some ghc extensions (with dependent types)
+   
diff --git a/haskell/types.hs b/haskell/types.hs
new file mode 100644
index 0000000..ce2a0cd
--- /dev/null
+++ b/haskell/types.hs
@@ -0,0 +1,83 @@
+{-# 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))))