[2] https://hackage.haskell.org/package/shakespeare

Cheers
Melanie Brown

On Fri, Dec 8, 2023 at 15:31, Adam Gundry <adam@well-typed.com> 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.