[Haskell-cafe] OverloadedStrings, but with compile-time invariants

[Melanie Brown]

You can achieve this with Template Haskell in multiple ways; one mentioned already by Viktor with $$(splices), and another way with [special|quasiquotes|]. A quasiquoter [1] (in this example, “special”) lets you specify the way its body (the stuff between the separators) gets translated into source code by the compiler with complex intermediate steps like parsing and interpolation.

An excellent example of the strength of quasiquoters is the shakespeare library [2] used by Yesod: though it is mainly for HTML/CSS/JS templating, I often use the “st” quasiquoter instead of -XOverloadedStrings to get around ambiguity errors. I’ve made my own quasiquoter imitating the Yesod library for interpolating Haskell values into raw SQL code following those examples. I think it would be fairly simple to write one for a NonEmptyText type, especially if you don’t need variable interpolation.

[1] https://hackage.haskell.org/package/template-haskell-2.21.0.0/docs/Language-Haskell-TH-Quote.html#t:QuasiQuoter
[2] https://hackage.haskell.org/package/shakespeare

Cheers
Melanie Brown

On Fri, Dec 8, 2023 at 15:31, Adam Gundry <[adam at well-typed.com](mailto:On Fri, Dec 8, 2023 at 15:31, Adam Gundry <<a href=)> wrote:

> Hi Max,
>
> Since GHC 9.6 you can do this with OverloadedLabels, at the minor
> syntactic cost of a prefix # on the literal. For example:
>
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE OverloadedLabels #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE UndecidableInstances #-}
>
> import Data.Kind
> import Data.Proxy
> import GHC.OverloadedLabels
> import GHC.TypeError
> import GHC.TypeLits
>
> newtype NonEmptyString = NonEmptyString String
>
> type family MyInvariant (s :: Symbol) :: Constraint where
> MyInvariant "" = Unsatisfiable ('Text "Empty string literal")
> MyInvariant _s = ()
>
> instance (MyInvariant lit, KnownSymbol lit)
> => IsLabel lit NonEmptyString where
> fromLabel = NonEmptyString (symbolVal (Proxy @lit))
>
> good, bad :: NonEmptyString
> good = #"A b c"
> bad = #""
> {-
> • Empty string literal
> • In the expression: #"" :: NonEmptyString
> In an equation for ‘bad’: bad = #"" :: NonEmptyString
> -}
>
> More details are in the proposal:
> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0170-unrestricted-overloadedlabels.rst
>
> Cheers,
>
> Adam
>
> On 08/12/2023 15:50, Max Ulidtko wrote:
>> Greetings @cafe,
>>
>> Transparent wrapping of string literals into custom types, driven
>> automatically by type inference, is of course very useful. I'm getting
>> huge mileage off GHC's OverloadedStrings when working with e.g. the Text
>> type:
>>
>> class IsString a where
>> fromString :: String -> a
>>
>>
>> instance IsString Text {- ... -}
>>
>>
>> greeting :: Text
>>
>> greeting = "Hello"
>>
>>
>> But I hope there's possibly room for improvement. I've got a bag of
>> several use-cases; perhaps the simplest is the following.
>>
>> Consider a type called NonEmptyText which is a (wrapper around) Text,
>> but with an added invariant that the contained text is never the empty
>> string "".
>>
>> Depending on codebase, such a type can be very useful too, allowing to
>> offload the burden of keeping track of the invariant onto machine; the
>> typechecker will show me all the spots to handle, current or future
>> ones. IOW, this type enables writing a non-boolean-blind null check,
>> toNonEmptyText :: ToText str => str -> Maybe NonEmptyText — which makes
>> not only the programmer, but also the compiler, aware of the null-check
>> result.
>>
>> I'm focusing the example on Text to somewhat maintain generality of the
>> idea. NonEmpty Char can be an alternative formulation of "non-empty
>> String"; length-indexed vectors could possibly handle this too. But
>> there're all sorts of invariants besides non-emptiness one may wish to
>> express.
>>
>> I'll omit other examples; but to summarize, I've got plenty of practical
>> motivation to get "smart literals".
>>
>> And to the point: IsString as it stands, forces us to write much
>> unsatisfactory instances:
>>
>> instance IsString NonEmptyText where
>>
>> fromString (c:cs) = NonEmptyText.new c cs
>>
>> fromString [] = error "unavoidable runtime panic" -- argh
>>
>>
>> ... despite fromString being invoked, presumably with OverloadedStrings,
>> on a string literal — which is statically known at compile-time.
>>
>> I'd imagine upgrading the interface with GHC's own TypeLits:
>>
>> class KnownSymbol lit => IsString' str lit where
>>
>> fromString' :: proxy lit -> str
>>
>>
>> This 2-parameter formulation of IsString enables pretty straightforward
>> user code, along the lines of:
>>
>> type family MyInvariant (s :: Symbol) :: Constraint where
>> MyInvariant "" = TypeError ('Text "Empty string literal")
>> MyInvariant _s = ()
>>
>> instance (MyInvariant lit, KnownSymbol lit) => IsString' NonEmptyText
>> lit where
>> fromString' = nothingImpossible . NeT.fromText . toText . symbolVal where
>> nothingImpossible (Just x) = x
>> nothingImpossible Nothing = error "typelevel invariant violated"
>>
>> text1, text2 :: NonEmptyText
>> text1 = fromString' $ Proxy @"hello, types"
>> text2 = fromString' $ Proxy @"" -- compile error here, as
>> expected!
>>
>> With the primes, this is possible to write today. With
>> AllowAmbiguousTypes, the unwieldy syntax can be abbreviated somewhat,
>> e.g. smartLiteral @"overloaded string literal with compiler-checked
>> invariant" — but is still rather awkward... in the same way that
>> ubiquitous T.pack is annoying enough to want to enable OverloadedStrings
>> and stop seeing it all over the place.
>>
>> The question is, could this IsString' somehow become the IsString that
>> OverloadedStrings is friends with?
>> I guess, not soon, with compatibility in mind... But in principle? Is it
>> even worth trying to pursue the GHC Proposal path?
>> Perhaps a new extension OverloadedTypelevelStrings?
>>
>> Relatedly... Can a GHC Plugin do this?
>>
>> And overall, to zoom out of "XY Problem" pitfalls: am I missing a neater
>> way to have "partial" IsString instances, those that can reject some
>> literals at compile-time?
>>
>> Having this code work is the goal:
>>
>> text1, text2 :: NonEmptyText
>> text1 = "hello, types"
>> text2 = "" -- compile error
>>
>> Best regards,
>> Max
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, https://www.well-typed.com/
>
> Registered in England & Wales, OC335890
> 27 Old Gloucester Street, London WC1N 3AX, England
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20231210/17f5252f/attachment.html>