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

[Oleg Grenrus]

Can a ghc-plugin do that?

Yes, see 
https://hackage.haskell.org/package/overloaded-0.3.1/docs/Overloaded-Symbols.html

- Oleg

On 8.12.2023 17.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
>
> _______________________________________________
> 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/20231208/1b8d36db/attachment.html>