Ticket #13025: Rec.hs

File Rec.hs, 1.1 KB (added by acowley, 3 years ago)
Line 
1{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts,
2             FlexibleInstances, GADTs, MultiParamTypeClasses,
3             PolyKinds, ScopedTypeVariables, TypeFamilies,
4             TypeOperators #-}
5module Rec where
6
7data Nat = Z | S Nat
8data Proxy a = Proxy
9
10data Field :: (k,*) -> * where
11  Field :: a -> Field '(s,a)
12
13type family Index r rs :: Nat where
14  Index r (r ': rs) = 'Z
15  Index r (s ': rs) = 'S (Index r rs)
16
17data Rec (rs :: [ (k,*) ]) where
18  Nil :: Rec '[]
19  (:&) :: Field r -> Rec rs -> Rec (r ': rs)
20infixr 5 :&
21
22class Index r rs ~ i => HasField r rs i where
23  get :: proxy r -> Rec rs -> Field r
24  set :: Field r -> Rec rs -> Rec rs
25
26instance HasField r (r ': rs) 'Z where
27  get _ (x :& _) = x
28  set x (_ :& xs) = x :& xs
29
30instance (HasField r rs i, Index r (s ': rs) ~ 'S i)
31         => HasField r (s ': rs) ('S i) where
32  get p (_ :& xs) = get p xs
33  set x' (x :& xs) = x :& set x' xs
34
35type Has r rs = HasField r rs (Index r rs)
36
37getField :: Has '(s,a) rs => proxy '(s,a) -> Rec rs -> a
38getField p = aux . get p
39  where aux :: Field '(s,a) -> a
40        aux (Field x) = x