...
 
Commits (2)
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, UndecidableInstances, PolyKinds, DataKinds, GADTs #-}
module Ctf where
-----------------------------------------------------------------------
-- Goal: To familiarize with the syntax
-----------------------------------------------------------------------
-- Introduction: playing with unary numbers
data SZero = SZero
data SSucc b where { SSucc :: SNat b => b -> SSucc b }
class SNat n where
snatToInt :: n -> Int
instance SNat SZero where
snatToInt SZero = 0
instance (SNat n) => SNat (SSucc n) where
snatToInt (SSucc n) = 1 + snatToInt n
instance Show SZero where { show _ = "S0" }
instance (SNat n) => Show (SSucc n) where
show n = 'S' : (show $ snatToInt n)
-- with promotion Nat becomes a kind and Zero/Succ types with Nat kind (not *)
data Nat = Zero | Succ Nat deriving Show
type family Add (n :: Nat) (m :: Nat) :: Nat where
Add (Succ x) m = Succ (Add x m)
Add Zero m = m
-- going to and fro kinds and types
type family SNatLift (n :: *) :: Nat where
SNatLift SZero = Zero
SNatLift (SSucc n) = Succ (SNatLift n)
type family NatToSNat (n :: Nat) :: * where
NatToSNat Zero = SZero
NatToSNat (Succ n) = SSucc (NatToSNat n)
-- *Ctf> let x::NatToSNat (SNatLift (SSucc SZero)); x = undefined
-- *Ctf> :t x
-- x :: SSucc SZero
-- *Ctf> snatToInt x -- still computed at runtime even though the type should be enough
-- *** Exception: Prelude.undefined
-----------------------------------------------------------------------
-- Goal: Take a look at some more advanced use cases.
-----------------------------------------------------------------------
-- The paper says it uses OverlappingInstances flag,
-- however ghc gives us the following warning:
-- "-XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS"
type family Or (a :: Bool) (b :: Bool) :: Bool where
Or False False = False
Or a b = True
type family Equal (a :: *) (b :: *) :: Bool where
Equal a a = True
Equal a b = False
-- this is an example given in the paper
data Tree a = Leaf a | Branch (Tree a) (Tree a)
type family TMember (e :: *) (set :: Tree *) :: Bool where
TMember e (Leaf x) = Equal e x
TMember e (Branch l r) = Or (TMember e l) (TMember e r)
-- but I think this is more useful as it allows us to look inside a tree of types:
data Pair a b = Pair a b deriving Show
type family TMember' (e :: *) (set :: *) :: Bool where
TMember' e (Pair a b) = Or (TMember' e a) (TMember' e b)
-- or even pairs:
TMember' e (a,b) = Or (TMember' e a) (TMember' e b)
-- yes, overlapping instances for the bottom case:
TMember' e x = Equal e x
foo :: (TMember' Char a ~ True) => a -> a
foo x = x
-- callable with stuff like:
foores = foo ((23::Int, "hello"), ((3,4), (Pair (Pair 4 'e') 43)))
-----------------------------------------------------------------------
-- Next goal: Gain some practice with more drilling examples
-----------------------------------------------------------------------
-- another example for computation:
data Bin = Bin0 Bin | Bin1 Bin | BinZ deriving Show
type BinOne = Bin1 BinZ
type BinTwo = Bin0 BinOne -- 2 = ((1)<<1)+0
type BinThree = Bin1 BinOne -- 3 = ((1)<<1)+1
type BinFour = Bin0 BinTwo -- 4 = ((2)<<1)+0 = 1<<2
type BinFive = Bin1 BinTwo -- 5 = ((2)<<1)+1 -- 0b101
type BinSix = Bin0 BinThree -- 6 = 3*2+0
type BinSeven = Bin1 BinThree -- 7 = 3*2+1
type BinTwentyFive = Bin1 (Bin0 BinSix) -- 6*4+1
type family BinToUnary (n :: Bin) :: Nat where
BinToUnary (Bin1 x) = Succ (Add (BinToUnary x) (BinToUnary x))
BinToUnary (Bin0 x) = Add (BinToUnary x) (BinToUnary x)
BinToUnary BinZ = Zero
type family BinAdd (x :: Bin) (y :: Bin) :: Bin where
BinAdd BinZ y = y
BinAdd (Bin0 x) (Bin0 y) = Bin0 (BinAdd x y)
BinAdd (Bin0 x) (Bin1 y) = Bin1 (BinAdd x y)
BinAdd (Bin1 x) (Bin1 y) = Bin0 (BinAdd (BinAdd x y) BinOne)
-- BinAdd (BinDecr x) y = BinDecr (BinAdd x y) -- can't be added, will be explained later
-- BinAdd x (Bin1 y) = BinAdd BinZ (Bin1 y) -- even if we add a "matching" pattern it won't match (Candidate Rule 2?)
BinAdd x y = BinAdd y x
type family BinDecr (x :: Bin) :: Bin where
BinDecr (Bin1 BinZ) = BinZ -- can be added to avoid leading zeros
BinDecr (Bin1 x) = Bin0 x
BinDecr (Bin0 x) = Bin1 (BinDecr x)
type family BinSucc (n :: Bin) where
BinSucc n = BinAdd n BinOne
data SBinZ = SBinZ deriving Show
data SBin0 b = SBin0 b deriving Show
data SBin1 b = SBin1 b deriving Show
type family BinLift (n :: *) :: Bin where
BinLift SBinZ = BinZ
BinLift (SBin0 b) = Bin0 (BinLift b)
type family BinToSBin (n :: Bin) :: * where
BinToSBin BinZ = SBinZ
BinToSBin (Bin0 b) = SBin0 (BinToSBin b)
BinToSBin (Bin1 b) = SBin1 (BinToSBin b)
-----------------------------------------------------------------------
-- Goal of the following part: To explain the behaviour without getting into definitions.
-----------------------------------------------------------------------
-- what would happen if we try to type something as "-1"?
-- *Ctf> let x :: BinToSBin (BinAdd BinZ (BinDecr BinZ)); x=x
-- *Ctf> :t x
-- x :: BinToSBin (BinDecr 'BinZ)
-- what about (-1)+1?
-- let x :: BinToSBin (BinAdd (BinDecr BinZ) BinOne); x=x
-- time to explain BinDecr inside BinAdd, showing example 3.1 and how it could result in multiple different patterns being matched depending on whether the evaluation is done,
-- time for a fun example
type family Fib (n :: Bin) :: Bin where
Fib BinZ = BinZ
Fib BinOne = BinOne
Fib n = BinAdd (Fib (BinDecr n)) (Fib (BinDecr (BinDecr n)))
-- *Ctf> let x :: BinToSBin (Fib BinZ); x=x
-- *Ctf> :t x
-- x :: SBinZ
-- *Ctf> let x :: BinToSBin (Fib BinOne); x=x
-- *Ctf> :t x
-- x :: SBin1 SBinZ
-- *Ctf> let x :: BinToSBin (Fib BinTwo); x=x
-- exercise: guess what would happen here!
-- exercise 2: guess why has this happened!
-- exercise 3: fix it!
-- written in japanese to avoid spoilers: 終了出来るため、先行ゼロに対するルールを加えて!!!
fib25 = let fib n = if n<2 then n else fib (n-1) + fib (n-2) in fib 25
-- *Ctf> let x :: BinToSBin (Fib BinTwentyFive); x=x
-- *Ctf> :t x
-- Example 3.2
type family FunIf (b :: Bool) :: * where
FunIf True = Int -> Int
FunIf False = ()
--bad :: d -> FunIf (Equal Bool d)
--bad _ = ()
-- at this point we already have a compile error thrown at bad, as FunIf True case isn't handled.
-- Additional reading material:
-- * Type level strings:
-- https://kcsongor.github.io/symbol-parsing-haskell/
-- * Avoid overlapping instances issues with closed type families:
-- https://kseo.github.io/posts/2017-02-05-avoid-overlapping-instances-with-closed-type-families.html