overloadedlabelsrun02.hs 1.33 KB
Newer Older
Adam Gundry's avatar
Adam Gundry committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
-- Using overloaded labels to provide nice syntactic sugar for a
-- term representation using de Bruijn indices

{-# LANGUAGE OverloadedLabels
           , DataKinds
           , FlexibleContexts
           , FlexibleInstances
           , GADTs
           , KindSignatures
           , MultiParamTypeClasses
           , NoMonomorphismRestriction
           , OverlappingInstances
           , ScopedTypeVariables
           , StandaloneDeriving
           , TypeOperators
  #-}

import GHC.OverloadedLabels
import Data.Proxy ( Proxy(..) )
import GHC.TypeLits ( Symbol )

instance x ~ y => IsLabel x (Proxy y) where
  fromLabel _ = Proxy

data Elem (x :: Symbol) g where
  Top :: Elem x (x ': g)
  Pop :: Elem x g -> Elem x (y ': g)
deriving instance Show (Elem x g)


class IsElem x g where
  which :: Elem x g

instance IsElem x (x ': g) where
  which = Top

instance IsElem x g => IsElem x (y ': g) where
  which = Pop which


data Tm g where
  Var :: Elem x g -> Tm g
  App :: Tm g -> Tm g -> Tm g
  Lam :: Tm (x ': g) -> Tm g
deriving instance Show (Tm g)

instance IsElem x g => IsLabel x (Tm g) where
  fromLabel _ = Var (which :: Elem x g)

lam :: Proxy x -> Tm (x ': g) -> Tm g
lam _ = Lam

s = lam #x #x
t = lam #x (lam #y (#x `App` #y))

u :: IsElem "z" g => Tm g
u = #z `App` #z

main = do print s
          print t
          print (u :: Tm '["z"])