[Haskell-cafe] type level strings?

[oleg at okmij.org]

Evan Laforge has defined
> data Thing {
>   thing_id :: ThingId
>   , thing_stuff :: Stuff
>   }
> newtype ThingId = ThingId String

and wishes to statically preclude binary operations with things that
have different ThingIds. However, Things and their Ids can be loaded
from files and so cannot be known to the compiler. He wished for
type-level strings -- which is what the enclosed code gives.


When we've got two Things loaded from two different files we must do a
run-time check to see if these two things have in fact the same
ThingId. That is inevitable. The question is how frequently do we have
to make such a test?

One approach is to do such a ruin-time test on each binary operation
on things.  The original Thing above was of that approach:

> instance Monoid Thing where
>   mappend (Thing id1 stuff1) (Thing id2 stuff2)
>     | id1 /= id2 = error "..."
>     | otherwise = Thing id1 (stuff1 `mappend` stuff2)

Every time we mappend things, we must check their ids.

It has been suggested to use existentials. We get the the following code:

> maybeAppend :: Exists Thing -> Exists Thing -> Maybe (Exists Thing)
> maybeAppend (Exists t1) (Exists t2) =
>     case thing_id t1 `equal` thing_id t2 of
>       Just Refl -> Just $ Exists (t1 `mappend` t2)
>       Nothing   -> Nothing

How different is this from the original mappend? Every time we wish to
mappend two things, we have to do the run-time test of their ids!
We added phantom times, existentials, GADTs -- and got nothing in
return. No improvement to the original code, and no static guarantees.


When we have to mappend things several times, it seems optimal to do
the run-time ID check only once (we have to do that check anyway) and
then mappend the results without any checks, and with full static
assurance that only Identical things are mappended. The enclosed code
implements that approach. The instance for Monoid makes patent only
things with the same id may be mappended. Moreover, there is no
run-time id check, and we do not have to think up the id to give to
mempty. The test does read two things from a `file' (a string) and
does several operations on them. The run-time test is done only once.

The ideas of the code are described in the papers with Chung-chieh
Shan on lightweight static capabilities and implicit configurations.

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}

module Thing where

import Data.Monoid
import Data.Char

-- The data constructor Thing should not be exported
newtype Thing id = Thing{ thingStuff :: Stuff }

type Stuff = [Int]  -- or any monoid

class IDeal id where get_id :: id -> String

-- The user should use make_thing
make_thing :: IDeal id => id -> Stuff -> Thing id
make_thing _ t = Thing t

-- It is statically assured that only things with the same id
-- may be mappended. Moreover, there is no run-time id check
-- And we do not have to think up the id to give to mempty

instance Monoid (Thing id) where
    Thing t1 `mappend` Thing t2 = Thing (t1 `mappend` t2)
    mempty = Thing mempty

instance IDeal id => Show (Thing id) where
    show (Thing t) = show $ (get_id (undefined::id),t)

-- A statically-known Id (just in case)

data Id1 = Id1
instance IDeal Id1 where get_id _ = "Id1"

-- Reading a thing from a file (or at least, a string)

data DynId id = DynId
instance Nat id => IDeal (DynId id) where 
    get_id _ = int_to_str $ nat (undefined::id)

read_thing :: String -> (forall id. IDeal id => Thing id -> w) -> w
read_thing str k = reify_ideal i (\iD -> k (make_thing iD t))
  where (i,t) = read str 

-- Run-time equality check
-- If id and id' are the same, cast the second to the same id

eqid_check :: forall id id'. (IDeal id, IDeal id') => 
	      Thing id -> Thing id' -> Maybe (Thing id)
eqid_check _ (Thing t) | get_id (undefined::id) == get_id (undefined::id') 
    = Just (Thing t)
eqid_check _ _ = Nothing

test file1 file2 =
    read_thing file1 (\t1 ->
    read_thing file2 (\t2 ->
      do_things t1 t2))
 where
 -- A run-time test is inevitable, but it is done only once
 do_things t1 t2 | Just t2' <- eqid_check t1 t2 = do_things' t1 t2'
 do_things _ _ = error "bad things"

 -- Now it is assured we have the same id
 -- we can do things many times
 do_things' :: IDeal id => Thing id -> Thing id -> String 
 do_things' t1 t2 = show $
   mempty `mappend` t1 `mappend` t2 `mappend` t2 `mappend` t1

t1 = test "(\"id1\",[1,2])" "(\"id1\",[3,4])"
-- "(\"id1\",[1,2,3,4,3,4,1,2])"

t2 = test "(\"id1\",[1,2])" "(\"id2\",[3,4])"
-- "*** Exception: bad things


-- Reifying strings to types
-- They say String kinds are already in a GHC branch.
-- Edward Kmett maintains a Hackage package for these sort of things

-- Assume ASCII for simplicity
str_to_int :: String -> Integer
str_to_int "" = 0
str_to_int (c:t) = fromIntegral (ord c) + 128 * str_to_int t

int_to_str :: Integer -> String
int_to_str = loop ""
  where
  loop acc 0 = reverse acc
  loop acc n | (n',c) <- quotRem n 128 = loop (chr (fromIntegral c) : acc) n'

data Z = Z
data S a = S a
data T a = T a

class Nat a where nat :: a -> Integer
instance Nat Z where nat _ = 0
instance Nat a => Nat (S a) where nat _ = 1 + nat (undefined::a)
instance Nat a => Nat (T a) where nat _ = 2 * nat (undefined::a)

reify_integer :: Integer -> (forall x. Nat x => x -> w ) -> w
reify_integer 0 k = k Z
reify_integer n k | even n = reify_integer (n `div` 2) (\x -> k (T x))
reify_integer n k = reify_integer (n-1) (\x -> k (S x))

reify_ideal :: String -> (forall x. IDeal x => x -> w) -> w
reify_ideal str k = reify_integer (str_to_int str) (k . dynid)
 where dynid :: x -> DynId x
       dynid = undefined

tr1 = reify_integer 10 nat
tr2 = int_to_str $ reify_integer (str_to_int "id1") nat