[haskell] Try some ghc extensions
This commit is contained in:
parent
c3c94f3e35
commit
5685da9e7a
|
@ -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)
|
||||
|
||||
|
|
|
@ -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))))
|
Loading…
Reference in New Issue