CODEWITHSUNDEEP
haskellsingletondependent-type
user1198582
user1198582

Reputation:

Bringing "The Singletons Paper" up to date. How can I implement the AChar datatype using singleton library

Thanks to Benjamin Hodgson, I have started to implement a type-safe SQL-Interface, begun in this stackoverflow question.

As advised, I have started to read the singleton paper. I find that seeing working code helps a lot, and endeavored to see the supplied code work. However, the code is three years old, and needs some updating. Great! Now I get to learn something. Here's step one, removing the promoted type AChar with type-literal strings.

from the original code in singletons-examples/DatabaseStar.hs

{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# Language PolyKinds, DataKinds, TemplateHaskell, TypeFamilies,
    GADTs, TypeOperators, RankNTypes, FlexibleContexts, UndecidableInstances,
    FlexibleInstances, ScopedTypeVariables, MultiParamTypeClasses #-}

module DatabaseStar where

import Data.Singletons
import Data.Singletons.CustomStar
import Data.Singletons.TH

$(singletons [d|
-- A re-definition of Char as an algebraic data type.
-- This is necessary to allow for promotion and type-level Strings.
  data AChar = CA | CB | CC | CD | CE | CF | CG | CH | CI
             | CJ | CK | CL | CM | CN | CO | CP | CQ | CR
             | CS | CT | CU | CV | CW | CX | CY | CZ
             deriving (Read, Show, Eq)

-- A named attribute in our database
  data Attribute a = Attr [AChar] a

-- A schema is an ordered list of named attributes
  data Schema a = Sch [Attribute a]
  |]

I found AChar to be unsatisfying, and soon realized it was no longer needed.

But I am not sure how to implement type-level Strings for this use case. Could someone provide links for me to investigate, and/or hints.

Upvotes: 2

Views: 91

Answers (1)

Alec
Alec

Reputation: 32309

I believe type-level "strings" already exist - they go by the name Symbol.

ghci> :set +t -XTypeInType
ghci> import GHC.TypeLits
ghci> import Data.Proxy
ghci> Proxy :: Proxy "I'm a type level string!"
Proxy
it :: Proxy "I'm a type level string!"

That said, I think singleton still doesn't play well with these. The problem is that they lack string-like behaviour (like being able to extract characters or make a string from characters). I believe the best solution is still the ugly one of redeclaring characters.

Upvotes: 5

Related Questions