OverloadedStrings, but with compile-time invariants
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
Can a ghc-plugin do that? Yes, see https://hackage.haskell.org/package/overloaded-0.3.1/docs/Overloaded-Symbols... - 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.
On Fri, 8 Dec 2023, Max Ulidtko wrote:
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 "".
Maybe that is too much to expect from a string literal syntax? I have no convincing solution for your string example, but I got a nice one for general (non-Char) non-empty lists. Analogous to your example you might ask for overloaded list syntax for NonEmpty lists. We are so used to the list syntax with comma separation, that we have mostly forgotten about the list constructor (:). Instead of [1,2,3] we could write 1:2:3:[]. With this syntax it is also easy to write a type checked NonEmpty list this way: 1:|2:3:[]. With my non-empty package you can even write lists with any required minimum number of elements, like 1!:2!:3:4:5:[]. https://wiki.haskell.org/List_notation
On Fri, Dec 08, 2023 at 04:50:58PM +0100, Max Ulidtko wrote:
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
Is at TH splice too cumbersome? text1, text2 :: NonEmptyText text1 = $$(neTxt "hello, types") text = $$(neTxt "") -- compile error I am validating DNS domain name literals at compile time, where checks include full DNS syntax validation with no empty labels, no labels longer than 63 bytes, and overall wire length at most 255 bytes. https://github.com/dnsbase/dnsbase/blob/548270f2e575949592ca3f1e40c58edc450b... -- Viktor.
Might https://hackage.haskell.org/package/validated-literals be of interest?
On Fri, Dec 8, 2023 at 2:13 PM Viktor Dukhovni
On Fri, Dec 08, 2023 at 04:50:58PM +0100, Max Ulidtko wrote:
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
Is at TH splice too cumbersome?
text1, text2 :: NonEmptyText text1 = $$(neTxt "hello, types") text = $$(neTxt "") -- compile error
I am validating DNS domain name literals at compile time, where checks include full DNS syntax validation with no empty labels, no labels longer than 63 bytes, and overall wire length at most 255 bytes.
https://github.com/dnsbase/dnsbase/blob/548270f2e575949592ca3f1e40c58edc450b...
-- Viktor. _______________________________________________ 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.
-- brandon s allbery kf8nh allbery.b@gmail.com
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-un... 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
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-... [2] https://hackage.haskell.org/package/shakespeare Cheers Melanie Brown On Fri, Dec 8, 2023 at 15:31, Adam Gundry <[adam@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-un...
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.
participants (7)
-
Adam Gundry -
Brandon Allbery -
Henning Thielemann -
Max Ulidtko -
Melanie Brown -
Oleg Grenrus -
Viktor Dukhovni