Lib.hs

-- * Preamble

{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module Lib where

import           Control.Lens       (makeLenses)
import           Data.Default       (Default (..))
import           Data.Singletons.TH (genSingletons)
import           Data.Vinyl

-- * First Properties
-- Let's define some constructors for simple properties of the music we're
-- interested in:

newtype Loudness = Loudness Double
                 deriving (Eq, Show)

instance Default Loudness where
  def = Loudness 0

data Pitch = C | D | E | F | G | A | B deriving (Show)

-- * Vinyl Instances
-- Now, let's create some extensible records, using the vinyl library, based on
-- three proprieties of interest: the Volume and Pitch we saw before, and the idea
-- of Part, which is encoded as an integer (in a vocal fugue may be Bass, Tenor
-- etc)

data NoteProperty = Volume | Part | PitchValue deriving (Show, Ord, Eq)
genSingletons [''NoteProperty]

type FugueNote = Rec Attr ['Volume, 'Part, 'PitchValue]

type family Interpretation (np :: NoteProperty) :: * where
  Interpretation 'Volume     = Loudness
  Interpretation 'Part       = Int
  Interpretation 'PitchValue = Pitch

newtype Attr np = Attr { _unAttr :: Interpretation np }
makeLenses ''Attr

instance Show (Attr 'Volume)     where show (Attr x) = "volume: " ++ show x
instance Show (Attr 'Part)       where show (Attr x) = "part: " ++ show x
instance Show (Attr 'PitchValue) where show (Attr x) = "pitch: " ++ show x
instance Default (Interpretation a) => Default (Attr a) where def = Attr def

(=::) :: sing f -> Interpretation f -> Attr f
_ =:: x = Attr x

-- A simple note may be written in this setting as:
note :: FugueNote
note = (SVolume =:: Loudness 1) :& (SPart =:: 1) :& (SPitchValue =:: C) :& RNil

-- * The main problem
-- I'd like to be able to write "c" and mean the note which has pitch C and the
-- other fields as default ones. So I begin defining a typeclass:
class HasPitch (rs :: [NoteProperty]) where
  c :: Rec Attr rs
  d :: Rec Attr rs
  e :: Rec Attr rs
  f :: Rec Attr rs
  g :: Rec Attr rs
  a :: Rec Attr rs
  b :: Rec Attr rs

instance HasPitch '[] where
  c = RNil
  d = RNil
  e = RNil
  f = RNil
  g = RNil
  a = RNil
  b = RNil

instance {-# OVERLAPPING #-} HasPitch rs => HasPitch ('PitchValue ': rs) where
  c = (SPitchValue =:: C) :& c
  d = (SPitchValue =:: D) :& d
  e = (SPitchValue =:: E) :& e
  f = (SPitchValue =:: F) :& f
  g = (SPitchValue =:: G) :& g
  a = (SPitchValue =:: A) :& a
  b = (SPitchValue =:: B) :& b

instance (Default (Attr r), HasPitch rs) => HasPitch (r ': rs) where
  c = def :& c
  d = def :& d
  e = def :& e
  f = def :& f
  g = def :& g
  a = def :& a
  b = def :& b

-- Now I can have both:
littleScale :: [FugueNote]
littleScale = [c,d,e,f,a,b]

literalScale :: [Rec Attr '[PitchValue]]
literalScale = [c,d,e,f,a,b]

-- However, there are some problems with this approach. I could, for example, write:
nonSenseScale :: [Rec Attr '[]]
nonSenseScale = [c,d,e,f,a,b]

nonSenseScale2 :: [Rec Attr '[Volume]]
nonSenseScale2 = [c,d,e,f,a,b]

-- What I really wanted, instead, is the ability to have "c" mean something only in
-- the contexts in which my list of properties contains the PitchValue field, and
-- the other fields are default.