Skip to content

Instantly share code, notes, and snippets.

What would you like to do?

Compile Time Literals

I've been kicking an idea around for revamping overloaded literals in Haskell. Please give a thought:

Right now we do runtime fromInteger, fromString, fromList, etc. calls. The types of these functions are Integer -> a, String -> a, etc. These functions are usually partial for more interesting types, and the failure typically occurs at runtime. I propose that we convert the literal at compile-time instead (potentially using quasiquotes), along with new classes that provide function compileLiteral :: literal -> Either String value.

The definition would look like this:

class CompileInteger a where
  compileInteger :: Integer -> Either String a

So you could write:

instance CompileInteger Natural where
  compileInteger i
    | i < 0 = Left "Natural may not be negative"
    | otherwise = Right ...

When you enable CompileTimeLiterals (and NegativeLiterals), the definition:

x :: Natural
x = -3

would be desugared into:

x :: Natural
x = [compileIntegerE| -3 |]

which would then fail at compile time, noting exactly where the negative literal was introduced.

Another example: ByteString's IsString instance, which truncates Unicode characters per the documentation:

Manipulate ByteStrings using Char operations. All Chars will be truncated to 8 bits. It can be expected that these functions will run at identical speeds to their Word8 equivalents in Data.ByteString.

This can result in rather surprising behavior, all of which is uncovered only at runtime.

Using CompileTimeLiterals, we could provide a new implementation:

instance CompileString ByteString where
  compileString str
    | any ((> 255) . fromEnum) str = Left "Unicode characters present"
    | otherwise = Right (pack str)

This implementation provides a compile-time error rather than confusing runtime data.

We can provide an IsList instance to length-indexed vectors:

{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE FlexibleContexts   #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE GADTs              #-}
{-# LANGUAGE OverloadedLists    #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies       #-}

import           GHC.Exts

data Nat = Z | S Nat

data Vec i a where
    Nil :: Vec Z a
    Cons :: a -> Vec n a -> Vec (S n) a

deriving instance (Show a) => Show (Vec i a)

vecToList :: Vec i a -> [a]
vecToList Nil         = []
vecToList (Cons a as) = a : vecToList as

vtail :: Vec (S n) a -> Vec n a
vtail (Cons _ xs) = xs

instance IsList (Vec Z a) where
    type Item (Vec Z a) = a

    fromList [] = Nil
    fromList _  = error "nope"

    toList = vecToList

instance (IsList (Vec n a), Item (Vec n a) ~ a) => IsList (Vec (S n) a) where
    type Item (Vec (S n) a) = a

    fromList (x:xs) = Cons x (fromList xs)
    fromList _      = error "nope"

    toList = vecToList

But this instance is dangerous to use in practice, as the exception is buried lazily in the list.

λ> ['a', 'b', 'c'] :: Vec (S (S (S Z))) Char
Cons 'a' (Cons 'b' (Cons 'c' Nil))

λ> vtail ['a', 'b', 'c'] :: Vec (S (S (S Z))) Char
Cons 'b' (Cons 'c' *** Exception: nope
CallStack (from HasCallStack):
  error, called at /home/matt/olist.hs:33:18 in main:Main

With compile-time literals, this becomes a compile-time error, and OverloadedLists becomes safe to use with length-indexed vectors.

Another example is data NonEmpty a = a :| [a]. This can be given an IsList instance, but it is unsafe -- [] :: NonEmpty Int will fail at runtime whenever it is demanded.


This comment has been minimized.

Copy link
Owner Author

parsonsmatt commented Apr 17, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.