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.
Twitter thread: https://twitter.com/mattoflambda/status/986295093429600256