Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
20 messages Options
Reply | Threaded
Open this post in threaded view
|

Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Merijn Verstraaten
I've been repeatedly running into problems with overloaded literals and partial conversion functions, so I wrote up an initial proposal (https://ghc.haskell.org/trac/ghc/wiki/ValidateMonoLiterals) and I'd like to commence with the bikeshedding and hearing other opinions :)

Cheers,
Merijn

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

signature.asc (859 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

RE: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Simon Peyton Jones
I'm all for it.  Syntax sounds like the main difficulty.  Today you could use quasiquotatoin
        [even| 38 |]
and get the same effect as $$(validate 38).  But it's still noisy.

So: what is the non-noisy scheme you want to propose?  You don't quite get to that in the wiki page!

Simon

| -----Original Message-----
| From: ghc-devs [mailto:[hidden email]] On Behalf Of Merijn
| Verstraaten
| Sent: 05 February 2015 14:46
| To: [hidden email]; GHC users
| Subject: Proposal: ValidateMonoLiterals - Initial bikeshed discussion
|
| I've been repeatedly running into problems with overloaded literals and
| partial conversion functions, so I wrote up an initial proposal
| (https://ghc.haskell.org/trac/ghc/wiki/ValidateMonoLiterals) and I'd like
| to commence with the bikeshedding and hearing other opinions :)
|
| Cheers,
| Merijn
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Merijn Verstraaten
And no one of my proofreaders noticed that >.>

I would propose to have the extension replace the 'fromString "foo"', 'fromIntegral 5' and 'fromList [1,2,3]' calls (for monomorphic cases) in the AST with the relevant Typed TH splice.

I considered quasi-quotation initially too, but there's no quasi quotation syntax for Typed TH. I'm guessing that's just an oversight, but I'd really be in favour of adding a typed quasiquoter too. Similarly to thinking we should have an easier way to obtain Lift  instances since, to me at least, it seems that the Lift instance for most ADTs should be fairly trivial?

I'll quickly clarify the proposal on the wiki :)

Cheers,
Merijn

> On 5 Feb 2015, at 22:48, Simon Peyton Jones <[hidden email]> wrote:
>
> I'm all for it.  Syntax sounds like the main difficulty.  Today you could use quasiquotatoin
> [even| 38 |]
> and get the same effect as $$(validate 38).  But it's still noisy.
>
> So: what is the non-noisy scheme you want to propose?  You don't quite get to that in the wiki page!
>
> Simon
>
> | -----Original Message-----
> | From: ghc-devs [mailto:[hidden email]] On Behalf Of Merijn
> | Verstraaten
> | Sent: 05 February 2015 14:46
> | To: [hidden email]; GHC users
> | Subject: Proposal: ValidateMonoLiterals - Initial bikeshed discussion
> |
> | I've been repeatedly running into problems with overloaded literals and
> | partial conversion functions, so I wrote up an initial proposal
> | (https://ghc.haskell.org/trac/ghc/wiki/ValidateMonoLiterals) and I'd like
> | to commence with the bikeshedding and hearing other opinions :)
> |
> | Cheers,
> | Merijn

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

signature.asc (859 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Dominique Devriese-2
Merijn,

Perhaps only for the sake of discussion: have you considered doing
something at the type-level instead of using TH? I mean that you could
change the type of 42 from `forall a. Num a => a` to `forall a.
HasIntLiteral a '42 => a` where HasIntegerLiteral is a type class of
kind `* -> 'Integer -> Constraint` and people can instantiate it for
their types:

class HasIntegerLiteral (a :: *) (k :: 'Integer) where
  literal :: a

The desugarer could then just generate an invocation of "literal".

An advantage would be that you don't need TH (although you do need
DataKinds and type-level computation).  Specifically, type-checking
remains decidable and you can do it in safe haskell and so on.  I
haven't thought this through very far, so there may be other
advantages/disadvantages/glaring-holes-in-the-idea that I'm missing.

Regards,
Dominique

2015-02-06 11:07 GMT+01:00 Merijn Verstraaten <[hidden email]>:

> And no one of my proofreaders noticed that >.>
>
> I would propose to have the extension replace the 'fromString "foo"', 'fromIntegral 5' and 'fromList [1,2,3]' calls (for monomorphic cases) in the AST with the relevant Typed TH splice.
>
> I considered quasi-quotation initially too, but there's no quasi quotation syntax for Typed TH. I'm guessing that's just an oversight, but I'd really be in favour of adding a typed quasiquoter too. Similarly to thinking we should have an easier way to obtain Lift  instances since, to me at least, it seems that the Lift instance for most ADTs should be fairly trivial?
>
> I'll quickly clarify the proposal on the wiki :)
>
> Cheers,
> Merijn
>
>> On 5 Feb 2015, at 22:48, Simon Peyton Jones <[hidden email]> wrote:
>>
>> I'm all for it.  Syntax sounds like the main difficulty.  Today you could use quasiquotatoin
>>       [even| 38 |]
>> and get the same effect as $$(validate 38).  But it's still noisy.
>>
>> So: what is the non-noisy scheme you want to propose?  You don't quite get to that in the wiki page!
>>
>> Simon
>>
>> | -----Original Message-----
>> | From: ghc-devs [mailto:[hidden email]] On Behalf Of Merijn
>> | Verstraaten
>> | Sent: 05 February 2015 14:46
>> | To: [hidden email]; GHC users
>> | Subject: Proposal: ValidateMonoLiterals - Initial bikeshed discussion
>> |
>> | I've been repeatedly running into problems with overloaded literals and
>> | partial conversion functions, so I wrote up an initial proposal
>> | (https://ghc.haskell.org/trac/ghc/wiki/ValidateMonoLiterals) and I'd like
>> | to commence with the bikeshedding and hearing other opinions :)
>> |
>> | Cheers,
>> | Merijn
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Merijn Verstraaten
Hi Dominique,

I don't see how that would replace the usecase I describe? I'll give you a more concrete example from a library I'm working on. I'm working on a Haskell implementation of ZeroMQ, the ZMTP protocol lets sockets be named by a "binary identifier with length <= 255 and NOT starting with a NUL byte". As a programmer using this library I would have to write these socket identifiers in my source code. Now I have four options:

1) The library just doesn't validate identifiers to be compatible with the protocol (awful!)

2) My library produces a runtime error on every single invocation of the program (if it doesn't satisfy the constraints it will never successfully work)

3) I require a newtype'd input type with a smart constructor, which means the programmer still has to handle the "error" case even though it should never happen for literals written in the source.

4) Using a trick like what I desribed, the above newtype and smart constructor, and check at compile time that it is correct.

To be honest, I don't even see how your example would generalise to the rather trivial example using Even? For example, suppose we have "foo :: Even -> SomeData" how would I write "foo 2" using your idea in a way that, at compile time, checks that I'm not passing an invalid literal to foo?

As a further aside, your "type checking remains decidable" comment seems to imply that you think that type checking becomes undecidable with what I propose? Can you explain how that could be, considering that it already works in GHC, albeit in a very cumbersome way?

As for working with Safe Haskell, I'm all for better Safe Haskell support in TH, but unfortunately I'm already worried about my ability to tackle this proposal, let alone something more ambitious like making TH work better with Safe Haskell, I'll leave that task for someone more familiar with GHC.

Cheers,
Merijn

> On 6 Feb 2015, at 13:13, Dominique Devriese <[hidden email]> wrote:
>
> Merijn,
>
> Perhaps only for the sake of discussion: have you considered doing
> something at the type-level instead of using TH? I mean that you could
> change the type of 42 from `forall a. Num a => a` to `forall a.
> HasIntLiteral a '42 => a` where HasIntegerLiteral is a type class of
> kind `* -> 'Integer -> Constraint` and people can instantiate it for
> their types:
>
> class HasIntegerLiteral (a :: *) (k :: 'Integer) where
>  literal :: a
>
> The desugarer could then just generate an invocation of "literal".
>
> An advantage would be that you don't need TH (although you do need
> DataKinds and type-level computation).  Specifically, type-checking
> remains decidable and you can do it in safe haskell and so on.  I
> haven't thought this through very far, so there may be other
> advantages/disadvantages/glaring-holes-in-the-idea that I'm missing.
>
> Regards,
> Dominique
>
> 2015-02-06 11:07 GMT+01:00 Merijn Verstraaten <[hidden email]>:
>> And no one of my proofreaders noticed that >.>
>>
>> I would propose to have the extension replace the 'fromString "foo"', 'fromIntegral 5' and 'fromList [1,2,3]' calls (for monomorphic cases) in the AST with the relevant Typed TH splice.
>>
>> I considered quasi-quotation initially too, but there's no quasi quotation syntax for Typed TH. I'm guessing that's just an oversight, but I'd really be in favour of adding a typed quasiquoter too. Similarly to thinking we should have an easier way to obtain Lift  instances since, to me at least, it seems that the Lift instance for most ADTs should be fairly trivial?
>>
>> I'll quickly clarify the proposal on the wiki :)
>>
>> Cheers,
>> Merijn
>>
>>> On 5 Feb 2015, at 22:48, Simon Peyton Jones <[hidden email]> wrote:
>>>
>>> I'm all for it.  Syntax sounds like the main difficulty.  Today you could use quasiquotatoin
>>>      [even| 38 |]
>>> and get the same effect as $$(validate 38).  But it's still noisy.
>>>
>>> So: what is the non-noisy scheme you want to propose?  You don't quite get to that in the wiki page!
>>>
>>> Simon
>>>
>>> | -----Original Message-----
>>> | From: ghc-devs [mailto:[hidden email]] On Behalf Of Merijn
>>> | Verstraaten
>>> | Sent: 05 February 2015 14:46
>>> | To: [hidden email]; GHC users
>>> | Subject: Proposal: ValidateMonoLiterals - Initial bikeshed discussion
>>> |
>>> | I've been repeatedly running into problems with overloaded literals and
>>> | partial conversion functions, so I wrote up an initial proposal
>>> | (https://ghc.haskell.org/trac/ghc/wiki/ValidateMonoLiterals) and I'd like
>>> | to commence with the bikeshedding and hearing other opinions :)
>>> |
>>> | Cheers,
>>> | Merijn
>>
>>
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

signature.asc (859 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Adam Gundry-2
In reply to this post by Dominique Devriese-2
Hi Dominique,

On 06/02/15 12:13, Dominique Devriese wrote:

> Perhaps only for the sake of discussion: have you considered doing
> something at the type-level instead of using TH? I mean that you could
> change the type of 42 from `forall a. Num a => a` to `forall a.
> HasIntLiteral a '42 => a` where HasIntegerLiteral is a type class of
> kind `* -> 'Integer -> Constraint` and people can instantiate it for
> their types:
>
> class HasIntegerLiteral (a :: *) (k :: 'Integer) where
>   literal :: a
>
> The desugarer could then just generate an invocation of "literal".
>
> An advantage would be that you don't need TH (although you do need
> DataKinds and type-level computation).  Specifically, type-checking
> remains decidable and you can do it in safe haskell and so on.  I
> haven't thought this through very far, so there may be other
> advantages/disadvantages/glaring-holes-in-the-idea that I'm missing.

Interestingly, the string version of this would be remarkably similar to
the IV class [1] that came up in the redesign of OverloadedRecordFields:

    class IV (x :: Symbol) a where
      iv :: a

though in this case the plan was to have a special syntax for such
literals (e.g. #x).

It seems to me that what you would describe would work, and the
avoidance of TH is a merit, but the downside is the complexity of
implementing even relatively simple validation at the type level (as
opposed to just reusing a term-level function). For Merijn's Even
example I guess one could do something like this in current GHC:

    type family IsEven (n :: Nat) :: Bool where
      IsEven 0 = True
      IsEven 1 = False
      IsEven n = n - 2

    instance (KnownNat n, IsEven n ~ True)
            => HasIntegerLiteral Even n where
      literal = Even (natVal (Proxy :: Proxy n))

but anything interesting to do with strings (e.g. checking that
ByteStrings are ASCII) is rather out of reach at present.

Adam

[1]
https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Redesign#Implicitvalues


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Dominique Devriese-2
In reply to this post by Merijn Verstraaten
Hi Merijn,

2015-02-06 13:45 GMT+01:00 Merijn Verstraaten <[hidden email]>:
> I don't see how that would replace the usecase I describe?

I've written out the Even use case a bit, to hopefully clarify my
suggestion.  The code is a bit cumbersome and inefficient because I
can't use GHC type-lits because some type-level primitives seem to be
missing (modulo specifically).  Type-level Integers (i.e. a kind with
*negative* numbers and literals) would probably also be required for
an actual solution.

     {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, DataKinds,
KindSignatures, ExplicitForAll, PolyKinds, ScopedTypeVariables,
ConstraintKinds, TypeFamilies, GADTs, FlexibleContexts #-}

    module ValidateMonoLiterals where


    data Nat where
      Zero :: Nat
      Suc :: Nat -> Nat

    class KnownNat (n :: Nat) where
      natSing :: forall proxy. proxy n -> Integer

    instance KnownNat Zero where natSing _ = 0
    instance KnownNat k => KnownNat (Suc k) where natSing _ = natSing
(Proxy :: Proxy k) + 1

    data Proxy (t :: k) = Proxy

    class HasNatLiteral a (k :: Nat) where
      literal :: Proxy k -> a

    data Even = Even Integer

    class CheckEven (k :: Nat) where
    instance CheckEven Zero
    instance CheckEven k => CheckEven (Suc (Suc k)) where

    instance (KnownNat k, CheckEven k) => HasNatLiteral Even (k :: Nat) where
      literal _ = Even (fromInteger (natSing (Proxy :: Proxy k)))

    instance (KnownNat k) => HasNatLiteral Integer k where
      literal _ = natSing (Proxy :: Proxy k)

    four :: HasNatLiteral n (Suc (Suc (Suc (Suc Zero)))) => n
    four = literal (Proxy :: Proxy (Suc (Suc (Suc (Suc Zero)))))

    three :: HasNatLiteral n (Suc (Suc (Suc Zero))) => n
    three = literal (Proxy :: Proxy (Suc (Suc (Suc Zero))))

    fourI :: Integer
    fourI = four

    fourEI :: Even
    fourEI = four

    -- fails with "No instance for CheckEven (Suc Zero)"
    -- threeEI :: Even
    -- threeEI = three

> I'll give you a more concrete example from a library I'm working on. I'm working on a Haskell implementation of ZeroMQ, the ZMTP protocol lets sockets be named by a "binary identifier with length <= 255 and NOT starting with a NUL byte". As a programmer using this library I would have to write these socket identifiers in my source code. Now I have four options:

> 1) The library just doesn't validate identifiers to be compatible with the protocol (awful!)
>
> 2) My library produces a runtime error on every single invocation of the program (if it doesn't satisfy the constraints it will never successfully work)
>
> 3) I require a newtype'd input type with a smart constructor, which means the programmer still has to handle the "error" case even though it should never happen for literals written in the source.
>
> 4) Using a trick like what I desribed, the above newtype and smart constructor, and check at compile time that it is correct.

Well, I think my suggestion could be used as another alternative. As I
mentioned, the compiler could translate the literal 42 to an
appropriately typed invocation of HasNatLiteral.literal, so that you
could also just write 42 but get the additional compile-time checking.

> To be honest, I don't even see how your example would generalise to the rather trivial example using Even? For example, suppose we have "foo :: Even -> SomeData" how would I write "foo 2" using your idea in a way that, at compile time, checks that I'm not passing an invalid literal to foo?

See above: the type of foo doesn't change w.r.t. your approach.

> As a further aside, your "type checking remains decidable" comment seems to imply that you think that type checking becomes undecidable with what I propose? Can you explain how that could be, considering that it already works in GHC, albeit in a very cumbersome way?

What I mean is that meta-programs invoked through TH can always fail
to terminate
(even though the ones you are using in your example are terminating).
Consider what happens if you change the definition of your validate to
this (or someone else implements your validateInteger like this for a
type):
  validate :: forall a . Validate a => Integer -> Q (TExp a)
  validate i = validate (i+1)

Regards,
Dominique
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Dominique Devriese-2
In reply to this post by Adam Gundry-2
2015-02-06 14:20 GMT+01:00 Adam Gundry <[hidden email]>:

> It seems to me that what you would describe would work, and the
> avoidance of TH is a merit, but the downside is the complexity of
> implementing even relatively simple validation at the type level (as
> opposed to just reusing a term-level function). For Merijn's Even
> example I guess one could do something like this in current GHC:
>
>     type family IsEven (n :: Nat) :: Bool where
>       IsEven 0 = True
>       IsEven 1 = False
>       IsEven n = n - 2
>
>     instance (KnownNat n, IsEven n ~ True)
>             => HasIntegerLiteral Even n where
>       literal = Even (natVal (Proxy :: Proxy n))
>
> but anything interesting to do with strings (e.g. checking that
> ByteStrings are ASCII) is rather out of reach at present.

Agreed.  For the idea to scale, good support for type-level
programming with Integers/Strings/... is essential.  Something else
that would be useful is an unsatisfiable primitive constraint
constructor `UnsatisfiableConstraint :: String -> Constraint` that can
be used to generate custom error messages. Then one could write
something like

  type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
  type family MustBeTrue True _ = ()
  type family MustBeTrue False error = UnsatisfiableConstraint error

  type family MustBeEven (n :: Nat) :: Constraint
  type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
literal :'" ++ show n ++ "' is not even!")

  instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...

Regards,
Dominique
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Erik Hesselink
On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
<[hidden email]> wrote:

> Agreed.  For the idea to scale, good support for type-level
> programming with Integers/Strings/... is essential.  Something else
> that would be useful is an unsatisfiable primitive constraint
> constructor `UnsatisfiableConstraint :: String -> Constraint` that can
> be used to generate custom error messages. Then one could write
> something like
>
>   type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
>   type family MustBeTrue True _ = ()
>   type family MustBeTrue False error = UnsatisfiableConstraint error
>
>   type family MustBeEven (n :: Nat) :: Constraint
>   type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
> literal :'" ++ show n ++ "' is not even!")
>
>   instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...

Note that there is a trick to fake this with current GHC: you can
write an equality constraint that is false, involving the type level
string:

>   type family MustBeTrue False error = (() ~ error)

Erik
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Merijn Verstraaten
While I am certainly in favour of better and more flexible approaches to enforcing this in the type system (I'm a big fan of all the dependent Haskell/singletons stuff), I don't think this is an appropriate solution here.

First off, a lot of interesting and important cases can't feasibly be solved right now (i.e., most things involving strings/lists). More importantly, I think the examples given in this thread so far are FAR beyond the capabilities of beginner/intermediate haskellers, whereas implementing a terminating "String -> Maybe a" is fairly trivial.

So in terms of pragmatical usability I think the TH approach is easier to implement in GHC, easier to use by end users and more flexible and powerful than the suggested type families/DataKinds.

I'm all in favour of some of the below directions, but pragmatically I think it'll be a while before any of those problems are usable by any beginners.

I also realise a lot of people prefer avoiding TH if at all possible, but given that this is an extension that people have to opt into that won't otherwise affect their code, I think that's acceptable. Personally, I'd gladly use TH in exchange for this sort of checking and I've talked to several others that would to.

Cheers,
Merijn

> On 6 Feb 2015, at 14:55, Erik Hesselink <[hidden email]> wrote:
>
> On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
> <[hidden email]> wrote:
>> Agreed.  For the idea to scale, good support for type-level
>> programming with Integers/Strings/... is essential.  Something else
>> that would be useful is an unsatisfiable primitive constraint
>> constructor `UnsatisfiableConstraint :: String -> Constraint` that can
>> be used to generate custom error messages. Then one could write
>> something like
>>
>>  type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
>>  type family MustBeTrue True _ = ()
>>  type family MustBeTrue False error = UnsatisfiableConstraint error
>>
>>  type family MustBeEven (n :: Nat) :: Constraint
>>  type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
>> literal :'" ++ show n ++ "' is not even!")
>>
>>  instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...
>
> Note that there is a trick to fake this with current GHC: you can
> write an equality constraint that is false, involving the type level
> string:
>
>>  type family MustBeTrue False error = (() ~ error)
>
> Erik
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

signature.asc (859 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Ryan Trinkle-3
In reply to this post by Erik Hesselink
I think the idea of compile-time validation for overloaded literals is fantastic, and doing it with nicer syntax than quasiquoting would really improve things.  However, I'm a bit confused about specifically how the requirement that it be monomorphic will play into this.  For example, if I have:

x = 1

Presumably this will compile, and give a run-time error if I ever instantiate its type to Even.  However, if I have:

x :: Even
x = 1

it will fail to compile?  Furthermore, if I have the former, and type inference determines that its type is Even, it sounds like that will also fail to compile, but if type inference determines that its type is forall a. Nat a => a, then it will successfully compile and then fail at runtime.

Am I understanding this correctly?


Ryan

On Fri, Feb 6, 2015 at 8:55 AM, Erik Hesselink <[hidden email]> wrote:
On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
<[hidden email]> wrote:
> Agreed.  For the idea to scale, good support for type-level
> programming with Integers/Strings/... is essential.  Something else
> that would be useful is an unsatisfiable primitive constraint
> constructor `UnsatisfiableConstraint :: String -> Constraint` that can
> be used to generate custom error messages. Then one could write
> something like
>
>   type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
>   type family MustBeTrue True _ = ()
>   type family MustBeTrue False error = UnsatisfiableConstraint error
>
>   type family MustBeEven (n :: Nat) :: Constraint
>   type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
> literal :'" ++ show n ++ "' is not even!")
>
>   instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...

Note that there is a trick to fake this with current GHC: you can
write an equality constraint that is false, involving the type level
string:

>   type family MustBeTrue False error = (() ~ error)

Erik
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Merijn Verstraaten
Ryan,

Unfortunately, yes, you are understanding that correctly.

The reason I qualified it with "monomorphic only" is that, I want to avoid breakage that would render the extension practically unusable in real code.

Let's say I right now have:

foo :: Num a => [a] -> [a]
foo = map (+1)

I have two options 1) we compile this as currently using fromIntegral and it WILL break for Even or 2) we reject any polymorphic use of literals like this. Given the amount of numerical code relying on the polymorphism of Num, I think the option of not being able to compile Num polymorphic code is completely out of the question. Almost no application  would work.

I would advocate in favour of not requiring an IsList/IsString instance for the validation class, this would allow you to write a conversion that ONLY converts literals in a validated way and will never successfully convert literals without the extension, since with the extension disabled GHC would try to use the fromList/fromString from the IsString/IsList classes which do not exist.

Unfortunately, given how deeply fromIntegral is tied to the Num class I don't see any way to achieve the same for Num. The only option would be to not make Even an instance of Num, that way the same trick as above could work. Removing fromIntegral from Num is obviously not going to happen and without doing that I don't see how we could prevent someone using fromIntegral manually to convert to Even in a way that won't break Num polymorphic functions. If you have any ideas on how to tackle this, I'm all open to hearing them!

I agree with you that this is ugly, but I console myself with the thought that being able to check all monomorphic literals is already a drastic improvement over the current state. And in the case of lists and strings we could actually ensure that things work well, since almost no one writes "IsString polymorphic" code.

Cheers,
Merijn

> On 6 Feb 2015, at 16:59, Ryan Trinkle <[hidden email]> wrote:
>
> I think the idea of compile-time validation for overloaded literals is fantastic, and doing it with nicer syntax than quasiquoting would really improve things.  However, I'm a bit confused about specifically how the requirement that it be monomorphic will play into this.  For example, if I have:
>
> x = 1
>
> Presumably this will compile, and give a run-time error if I ever instantiate its type to Even.  However, if I have:
>
> x :: Even
> x = 1
>
> it will fail to compile?  Furthermore, if I have the former, and type inference determines that its type is Even, it sounds like that will also fail to compile, but if type inference determines that its type is forall a. Nat a => a, then it will successfully compile and then fail at runtime.
>
> Am I understanding this correctly?
>
>
> Ryan
>
> On Fri, Feb 6, 2015 at 8:55 AM, Erik Hesselink <[hidden email]> wrote:
> On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
> <[hidden email]> wrote:
> > Agreed.  For the idea to scale, good support for type-level
> > programming with Integers/Strings/... is essential.  Something else
> > that would be useful is an unsatisfiable primitive constraint
> > constructor `UnsatisfiableConstraint :: String -> Constraint` that can
> > be used to generate custom error messages. Then one could write
> > something like
> >
> >   type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
> >   type family MustBeTrue True _ = ()
> >   type family MustBeTrue False error = UnsatisfiableConstraint error
> >
> >   type family MustBeEven (n :: Nat) :: Constraint
> >   type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
> > literal :'" ++ show n ++ "' is not even!")
> >
> >   instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...
>
> Note that there is a trick to fake this with current GHC: you can
> write an equality constraint that is false, involving the type level
> string:
>
> >   type family MustBeTrue False error = (() ~ error)
>
> Erik
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

signature.asc (859 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Ryan Trinkle-3
My greatest concern here would be that, as an application is maintained, a literal might go from monomorphic to polymorphic, or vice versa, without anybody noticing.  It sounds like this could result in a value silently becoming partial, which would be a big problem for application stability; in the opposite case - a partial value becoming a compile-time error - I am somewhat less concerned, but it could still be confusing and disruptive.

I would prefer that there be some syntactic indication that I want my literal to be checked at compile time.  This syntax could also add whatever monomorphism requirement is needed, and then it would become a compile-time error for the value to become polymorphic.  I don't know nearly enough about the type system to know whether this is possible.

Also, it seems to me that it might not be so clean as "monomorphic" versus "polymorphic".  For example, suppose I have this:

newtype PostgresTableName s = PostgresTableName String

where 's' is a phantom type representing the DB schema that the name lives in.  The validation function is independent of the schema - it simply fails if there are illegal characters in the name, or if the name is too long.  So, ideally, ("foo\0bar" :: forall s. PostgresTableName s) would fail at compile time, despite being polymorphic.


Ryan

On Fri, Feb 6, 2015 at 11:16 AM, Merijn Verstraaten <[hidden email]> wrote:
Ryan,

Unfortunately, yes, you are understanding that correctly.

The reason I qualified it with "monomorphic only" is that, I want to avoid breakage that would render the extension practically unusable in real code.

Let's say I right now have:

foo :: Num a => [a] -> [a]
foo = map (+1)

I have two options 1) we compile this as currently using fromIntegral and it WILL break for Even or 2) we reject any polymorphic use of literals like this. Given the amount of numerical code relying on the polymorphism of Num, I think the option of not being able to compile Num polymorphic code is completely out of the question. Almost no application  would work.

I would advocate in favour of not requiring an IsList/IsString instance for the validation class, this would allow you to write a conversion that ONLY converts literals in a validated way and will never successfully convert literals without the extension, since with the extension disabled GHC would try to use the fromList/fromString from the IsString/IsList classes which do not exist.

Unfortunately, given how deeply fromIntegral is tied to the Num class I don't see any way to achieve the same for Num. The only option would be to not make Even an instance of Num, that way the same trick as above could work. Removing fromIntegral from Num is obviously not going to happen and without doing that I don't see how we could prevent someone using fromIntegral manually to convert to Even in a way that won't break Num polymorphic functions. If you have any ideas on how to tackle this, I'm all open to hearing them!

I agree with you that this is ugly, but I console myself with the thought that being able to check all monomorphic literals is already a drastic improvement over the current state. And in the case of lists and strings we could actually ensure that things work well, since almost no one writes "IsString polymorphic" code.

Cheers,
Merijn

> On 6 Feb 2015, at 16:59, Ryan Trinkle <[hidden email]> wrote:
>
> I think the idea of compile-time validation for overloaded literals is fantastic, and doing it with nicer syntax than quasiquoting would really improve things.  However, I'm a bit confused about specifically how the requirement that it be monomorphic will play into this.  For example, if I have:
>
> x = 1
>
> Presumably this will compile, and give a run-time error if I ever instantiate its type to Even.  However, if I have:
>
> x :: Even
> x = 1
>
> it will fail to compile?  Furthermore, if I have the former, and type inference determines that its type is Even, it sounds like that will also fail to compile, but if type inference determines that its type is forall a. Nat a => a, then it will successfully compile and then fail at runtime.
>
> Am I understanding this correctly?
>
>
> Ryan
>
> On Fri, Feb 6, 2015 at 8:55 AM, Erik Hesselink <[hidden email]> wrote:
> On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
> <[hidden email]> wrote:
> > Agreed.  For the idea to scale, good support for type-level
> > programming with Integers/Strings/... is essential.  Something else
> > that would be useful is an unsatisfiable primitive constraint
> > constructor `UnsatisfiableConstraint :: String -> Constraint` that can
> > be used to generate custom error messages. Then one could write
> > something like
> >
> >   type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
> >   type family MustBeTrue True _ = ()
> >   type family MustBeTrue False error = UnsatisfiableConstraint error
> >
> >   type family MustBeEven (n :: Nat) :: Constraint
> >   type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
> > literal :'" ++ show n ++ "' is not even!")
> >
> >   instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...
>
> Note that there is a trick to fake this with current GHC: you can
> write an equality constraint that is false, involving the type level
> string:
>
> >   type family MustBeTrue False error = (() ~ error)
>
> Erik
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Dan Doel
Assuming a separate syntax, I believe that the criterion would be as simple as ensuring that no ValidateFoo constraints are left outstanding. The syntax would add the relevant validate call, and type variables involved in a ValidateFoo constraint would not be generalizable, and would have to be defaulted or inferred from elsewhere, similar to the monomorphism restriction. I'm not sure how difficult that would be to implement.

I'm not terribly gung ho on this, though. It feels very ad hoc. Making validation vs. non-validation syntactic rather than just based on polymorphism seems somewhat less so, though; so I'd prefer that direction. Finding unused syntax is always a problem, of course.

On Fri, Feb 6, 2015 at 11:38 AM, Ryan Trinkle <[hidden email]> wrote:
My greatest concern here would be that, as an application is maintained, a literal might go from monomorphic to polymorphic, or vice versa, without anybody noticing.  It sounds like this could result in a value silently becoming partial, which would be a big problem for application stability; in the opposite case - a partial value becoming a compile-time error - I am somewhat less concerned, but it could still be confusing and disruptive.

I would prefer that there be some syntactic indication that I want my literal to be checked at compile time.  This syntax could also add whatever monomorphism requirement is needed, and then it would become a compile-time error for the value to become polymorphic.  I don't know nearly enough about the type system to know whether this is possible.

Also, it seems to me that it might not be so clean as "monomorphic" versus "polymorphic".  For example, suppose I have this:

newtype PostgresTableName s = PostgresTableName String

where 's' is a phantom type representing the DB schema that the name lives in.  The validation function is independent of the schema - it simply fails if there are illegal characters in the name, or if the name is too long.  So, ideally, ("foo\0bar" :: forall s. PostgresTableName s) would fail at compile time, despite being polymorphic.


Ryan

On Fri, Feb 6, 2015 at 11:16 AM, Merijn Verstraaten <[hidden email]> wrote:
Ryan,

Unfortunately, yes, you are understanding that correctly.

The reason I qualified it with "monomorphic only" is that, I want to avoid breakage that would render the extension practically unusable in real code.

Let's say I right now have:

foo :: Num a => [a] -> [a]
foo = map (+1)

I have two options 1) we compile this as currently using fromIntegral and it WILL break for Even or 2) we reject any polymorphic use of literals like this. Given the amount of numerical code relying on the polymorphism of Num, I think the option of not being able to compile Num polymorphic code is completely out of the question. Almost no application  would work.

I would advocate in favour of not requiring an IsList/IsString instance for the validation class, this would allow you to write a conversion that ONLY converts literals in a validated way and will never successfully convert literals without the extension, since with the extension disabled GHC would try to use the fromList/fromString from the IsString/IsList classes which do not exist.

Unfortunately, given how deeply fromIntegral is tied to the Num class I don't see any way to achieve the same for Num. The only option would be to not make Even an instance of Num, that way the same trick as above could work. Removing fromIntegral from Num is obviously not going to happen and without doing that I don't see how we could prevent someone using fromIntegral manually to convert to Even in a way that won't break Num polymorphic functions. If you have any ideas on how to tackle this, I'm all open to hearing them!

I agree with you that this is ugly, but I console myself with the thought that being able to check all monomorphic literals is already a drastic improvement over the current state. And in the case of lists and strings we could actually ensure that things work well, since almost no one writes "IsString polymorphic" code.

Cheers,
Merijn

> On 6 Feb 2015, at 16:59, Ryan Trinkle <[hidden email]> wrote:
>
> I think the idea of compile-time validation for overloaded literals is fantastic, and doing it with nicer syntax than quasiquoting would really improve things.  However, I'm a bit confused about specifically how the requirement that it be monomorphic will play into this.  For example, if I have:
>
> x = 1
>
> Presumably this will compile, and give a run-time error if I ever instantiate its type to Even.  However, if I have:
>
> x :: Even
> x = 1
>
> it will fail to compile?  Furthermore, if I have the former, and type inference determines that its type is Even, it sounds like that will also fail to compile, but if type inference determines that its type is forall a. Nat a => a, then it will successfully compile and then fail at runtime.
>
> Am I understanding this correctly?
>
>
> Ryan
>
> On Fri, Feb 6, 2015 at 8:55 AM, Erik Hesselink <[hidden email]> wrote:
> On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
> <[hidden email]> wrote:
> > Agreed.  For the idea to scale, good support for type-level
> > programming with Integers/Strings/... is essential.  Something else
> > that would be useful is an unsatisfiable primitive constraint
> > constructor `UnsatisfiableConstraint :: String -> Constraint` that can
> > be used to generate custom error messages. Then one could write
> > something like
> >
> >   type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
> >   type family MustBeTrue True _ = ()
> >   type family MustBeTrue False error = UnsatisfiableConstraint error
> >
> >   type family MustBeEven (n :: Nat) :: Constraint
> >   type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
> > literal :'" ++ show n ++ "' is not even!")
> >
> >   instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n where ...
>
> Note that there is a trick to fake this with current GHC: you can
> write an equality constraint that is false, involving the type level
> string:
>
> >   type family MustBeTrue False error = (() ~ error)
>
> Erik
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Adam Gundry-2
If we go for a separate syntax, what do we gain over normal quasiquotes
or $$(validate x)? Sure, literals could be made a little more beautiful,
but I'm not sure it justifies stealing more syntax (and what would that
syntax be?).

Without a separate syntax, I'm not sure I understand the original
proposal. The wiki page says "GHC would replace
fromString/fromInteger/fromList expressions originating from literals
with a Typed TH splice along the lines of validate for all monomorphic
cases." What does "all monomorphic cases" mean? Is the idea what GHC
would typecheck an expression involving a literal integer, determine
that the occurrence had type Even, then evaluate the TH splice *after*
typechecking? Whereas if the occurrence had a non-ground type, it would
do something else?

None of this is particularly persuasive, I'm afraid. Is it worthwhile
introducing something new just to avoid having to write a quasiquote?

I *am* attracted to the idea of indexed classes in place of IsString/Num

  class KnownSymbol s => IsIndexedString (a :: *) (s :: Symbol) where
    fromIndexedString :: a

  class KnownInteger i => IsIndexedInteger (a :: *) (i :: Integer) where
     fromIndexedInteger :: a

These have a smooth upgrade path from the existing class instances via

    default fromIndexedString :: (KnownSymbol s, IsString a) => a
    fromIndexedString = fromString (symbolVal (Proxy :: Proxy s))

    default fromIndexedInteger :: (KnownInteger i, Num a) => a
    fromIndexedInteger = fromInteger (integerVal (Proxy :: Proxy i))

and other instances can take advantage of the additional type
information. perhaps we need to bring Dependent Haskell a bit closer
before this is justifiable...

Adam


On 06/02/15 17:24, Dan Doel wrote:

> Assuming a separate syntax, I believe that the criterion would be as
> simple as ensuring that no ValidateFoo constraints are left outstanding.
> The syntax would add the relevant validate call, and type variables
> involved in a ValidateFoo constraint would not be generalizable, and
> would have to be defaulted or inferred from elsewhere, similar to the
> monomorphism restriction. I'm not sure how difficult that would be to
> implement.
>
> I'm not terribly gung ho on this, though. It feels very ad hoc. Making
> validation vs. non-validation syntactic rather than just based on
> polymorphism seems somewhat less so, though; so I'd prefer that
> direction. Finding unused syntax is always a problem, of course.


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Evan Laforge
In reply to this post by Dan Doel
Would it be feasible to make a lighter-weight mode for quasiquotes
that doesn't require the whole "load the module in ghci" runaround?
If it didn't need to do that, there wouldn't be much downside to
turning it on everywhere.  And it would enable lots of QQ conveniences
that at least I don't think its worth enabling TH for, due to the ghci
hassle.

Greg Weber recently asked for input on the idea of restricted TH
modes, this seems related.

If a splice was pure and had no non-Prelude dependencies, could it be
run without ghci loading and stage restrictions?

I think it's really awkward how numeric literals use fromInteger and
fromRational, and those functions are grouped into Num and Fractional.
So if you want to use (+), you also have to accept literals, which
means you have to accept anything anyone might type.  Has there been
any kind of proposal to split fromInteger and fromRational into their
own typeclasses analogous to IsString?

On Fri, Feb 6, 2015 at 9:24 AM, Dan Doel <[hidden email]> wrote:

> Assuming a separate syntax, I believe that the criterion would be as simple
> as ensuring that no ValidateFoo constraints are left outstanding. The syntax
> would add the relevant validate call, and type variables involved in a
> ValidateFoo constraint would not be generalizable, and would have to be
> defaulted or inferred from elsewhere, similar to the monomorphism
> restriction. I'm not sure how difficult that would be to implement.
>
> I'm not terribly gung ho on this, though. It feels very ad hoc. Making
> validation vs. non-validation syntactic rather than just based on
> polymorphism seems somewhat less so, though; so I'd prefer that direction.
> Finding unused syntax is always a problem, of course.
>
> On Fri, Feb 6, 2015 at 11:38 AM, Ryan Trinkle <[hidden email]>
> wrote:
>>
>> My greatest concern here would be that, as an application is maintained, a
>> literal might go from monomorphic to polymorphic, or vice versa, without
>> anybody noticing.  It sounds like this could result in a value silently
>> becoming partial, which would be a big problem for application stability; in
>> the opposite case - a partial value becoming a compile-time error - I am
>> somewhat less concerned, but it could still be confusing and disruptive.
>>
>> I would prefer that there be some syntactic indication that I want my
>> literal to be checked at compile time.  This syntax could also add whatever
>> monomorphism requirement is needed, and then it would become a compile-time
>> error for the value to become polymorphic.  I don't know nearly enough about
>> the type system to know whether this is possible.
>>
>> Also, it seems to me that it might not be so clean as "monomorphic" versus
>> "polymorphic".  For example, suppose I have this:
>>
>> newtype PostgresTableName s = PostgresTableName String
>>
>> where 's' is a phantom type representing the DB schema that the name lives
>> in.  The validation function is independent of the schema - it simply fails
>> if there are illegal characters in the name, or if the name is too long.
>> So, ideally, ("foo\0bar" :: forall s. PostgresTableName s) would fail at
>> compile time, despite being polymorphic.
>>
>>
>> Ryan
>>
>> On Fri, Feb 6, 2015 at 11:16 AM, Merijn Verstraaten
>> <[hidden email]> wrote:
>>>
>>> Ryan,
>>>
>>> Unfortunately, yes, you are understanding that correctly.
>>>
>>> The reason I qualified it with "monomorphic only" is that, I want to
>>> avoid breakage that would render the extension practically unusable in real
>>> code.
>>>
>>> Let's say I right now have:
>>>
>>> foo :: Num a => [a] -> [a]
>>> foo = map (+1)
>>>
>>> I have two options 1) we compile this as currently using fromIntegral and
>>> it WILL break for Even or 2) we reject any polymorphic use of literals like
>>> this. Given the amount of numerical code relying on the polymorphism of Num,
>>> I think the option of not being able to compile Num polymorphic code is
>>> completely out of the question. Almost no application  would work.
>>>
>>> I would advocate in favour of not requiring an IsList/IsString instance
>>> for the validation class, this would allow you to write a conversion that
>>> ONLY converts literals in a validated way and will never successfully
>>> convert literals without the extension, since with the extension disabled
>>> GHC would try to use the fromList/fromString from the IsString/IsList
>>> classes which do not exist.
>>>
>>> Unfortunately, given how deeply fromIntegral is tied to the Num class I
>>> don't see any way to achieve the same for Num. The only option would be to
>>> not make Even an instance of Num, that way the same trick as above could
>>> work. Removing fromIntegral from Num is obviously not going to happen and
>>> without doing that I don't see how we could prevent someone using
>>> fromIntegral manually to convert to Even in a way that won't break Num
>>> polymorphic functions. If you have any ideas on how to tackle this, I'm all
>>> open to hearing them!
>>>
>>> I agree with you that this is ugly, but I console myself with the thought
>>> that being able to check all monomorphic literals is already a drastic
>>> improvement over the current state. And in the case of lists and strings we
>>> could actually ensure that things work well, since almost no one writes
>>> "IsString polymorphic" code.
>>>
>>> Cheers,
>>> Merijn
>>>
>>> > On 6 Feb 2015, at 16:59, Ryan Trinkle <[hidden email]> wrote:
>>> >
>>> > I think the idea of compile-time validation for overloaded literals is
>>> > fantastic, and doing it with nicer syntax than quasiquoting would really
>>> > improve things.  However, I'm a bit confused about specifically how the
>>> > requirement that it be monomorphic will play into this.  For example, if I
>>> > have:
>>> >
>>> > x = 1
>>> >
>>> > Presumably this will compile, and give a run-time error if I ever
>>> > instantiate its type to Even.  However, if I have:
>>> >
>>> > x :: Even
>>> > x = 1
>>> >
>>> > it will fail to compile?  Furthermore, if I have the former, and type
>>> > inference determines that its type is Even, it sounds like that will also
>>> > fail to compile, but if type inference determines that its type is forall a.
>>> > Nat a => a, then it will successfully compile and then fail at runtime.
>>> >
>>> > Am I understanding this correctly?
>>> >
>>> >
>>> > Ryan
>>> >
>>> > On Fri, Feb 6, 2015 at 8:55 AM, Erik Hesselink <[hidden email]>
>>> > wrote:
>>> > On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
>>> > <[hidden email]> wrote:
>>> > > Agreed.  For the idea to scale, good support for type-level
>>> > > programming with Integers/Strings/... is essential.  Something else
>>> > > that would be useful is an unsatisfiable primitive constraint
>>> > > constructor `UnsatisfiableConstraint :: String -> Constraint` that
>>> > > can
>>> > > be used to generate custom error messages. Then one could write
>>> > > something like
>>> > >
>>> > >   type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
>>> > >   type family MustBeTrue True _ = ()
>>> > >   type family MustBeTrue False error = UnsatisfiableConstraint error
>>> > >
>>> > >   type family MustBeEven (n :: Nat) :: Constraint
>>> > >   type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
>>> > > literal :'" ++ show n ++ "' is not even!")
>>> > >
>>> > >   instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n
>>> > > where ...
>>> >
>>> > Note that there is a trick to fake this with current GHC: you can
>>> > write an equality constraint that is false, involving the type level
>>> > string:
>>> >
>>> > >   type family MustBeTrue False error = (() ~ error)
>>> >
>>> > Erik
>>> > _______________________________________________
>>> > Glasgow-haskell-users mailing list
>>> > [hidden email]
>>> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>
>>> _______________________________________________
>>> Glasgow-haskell-users mailing list
>>> [hidden email]
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>
>>
>>
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Carter Schonwald

Its worth pointing out that when / if luites out of process TH design happens for ghc, TH will be usable in cross compile builds of ghc as well. So we shouldn't let that constraint we have for now dictate future tooling ideas.

On Feb 6, 2015 3:50 PM, "Evan Laforge" <[hidden email]> wrote:
Would it be feasible to make a lighter-weight mode for quasiquotes
that doesn't require the whole "load the module in ghci" runaround?
If it didn't need to do that, there wouldn't be much downside to
turning it on everywhere.  And it would enable lots of QQ conveniences
that at least I don't think its worth enabling TH for, due to the ghci
hassle.

Greg Weber recently asked for input on the idea of restricted TH
modes, this seems related.

If a splice was pure and had no non-Prelude dependencies, could it be
run without ghci loading and stage restrictions?

I think it's really awkward how numeric literals use fromInteger and
fromRational, and those functions are grouped into Num and Fractional.
So if you want to use (+), you also have to accept literals, which
means you have to accept anything anyone might type.  Has there been
any kind of proposal to split fromInteger and fromRational into their
own typeclasses analogous to IsString?

On Fri, Feb 6, 2015 at 9:24 AM, Dan Doel <[hidden email]> wrote:
> Assuming a separate syntax, I believe that the criterion would be as simple
> as ensuring that no ValidateFoo constraints are left outstanding. The syntax
> would add the relevant validate call, and type variables involved in a
> ValidateFoo constraint would not be generalizable, and would have to be
> defaulted or inferred from elsewhere, similar to the monomorphism
> restriction. I'm not sure how difficult that would be to implement.
>
> I'm not terribly gung ho on this, though. It feels very ad hoc. Making
> validation vs. non-validation syntactic rather than just based on
> polymorphism seems somewhat less so, though; so I'd prefer that direction.
> Finding unused syntax is always a problem, of course.
>
> On Fri, Feb 6, 2015 at 11:38 AM, Ryan Trinkle <[hidden email]>
> wrote:
>>
>> My greatest concern here would be that, as an application is maintained, a
>> literal might go from monomorphic to polymorphic, or vice versa, without
>> anybody noticing.  It sounds like this could result in a value silently
>> becoming partial, which would be a big problem for application stability; in
>> the opposite case - a partial value becoming a compile-time error - I am
>> somewhat less concerned, but it could still be confusing and disruptive.
>>
>> I would prefer that there be some syntactic indication that I want my
>> literal to be checked at compile time.  This syntax could also add whatever
>> monomorphism requirement is needed, and then it would become a compile-time
>> error for the value to become polymorphic.  I don't know nearly enough about
>> the type system to know whether this is possible.
>>
>> Also, it seems to me that it might not be so clean as "monomorphic" versus
>> "polymorphic".  For example, suppose I have this:
>>
>> newtype PostgresTableName s = PostgresTableName String
>>
>> where 's' is a phantom type representing the DB schema that the name lives
>> in.  The validation function is independent of the schema - it simply fails
>> if there are illegal characters in the name, or if the name is too long.
>> So, ideally, ("foo\0bar" :: forall s. PostgresTableName s) would fail at
>> compile time, despite being polymorphic.
>>
>>
>> Ryan
>>
>> On Fri, Feb 6, 2015 at 11:16 AM, Merijn Verstraaten
>> <[hidden email]> wrote:
>>>
>>> Ryan,
>>>
>>> Unfortunately, yes, you are understanding that correctly.
>>>
>>> The reason I qualified it with "monomorphic only" is that, I want to
>>> avoid breakage that would render the extension practically unusable in real
>>> code.
>>>
>>> Let's say I right now have:
>>>
>>> foo :: Num a => [a] -> [a]
>>> foo = map (+1)
>>>
>>> I have two options 1) we compile this as currently using fromIntegral and
>>> it WILL break for Even or 2) we reject any polymorphic use of literals like
>>> this. Given the amount of numerical code relying on the polymorphism of Num,
>>> I think the option of not being able to compile Num polymorphic code is
>>> completely out of the question. Almost no application  would work.
>>>
>>> I would advocate in favour of not requiring an IsList/IsString instance
>>> for the validation class, this would allow you to write a conversion that
>>> ONLY converts literals in a validated way and will never successfully
>>> convert literals without the extension, since with the extension disabled
>>> GHC would try to use the fromList/fromString from the IsString/IsList
>>> classes which do not exist.
>>>
>>> Unfortunately, given how deeply fromIntegral is tied to the Num class I
>>> don't see any way to achieve the same for Num. The only option would be to
>>> not make Even an instance of Num, that way the same trick as above could
>>> work. Removing fromIntegral from Num is obviously not going to happen and
>>> without doing that I don't see how we could prevent someone using
>>> fromIntegral manually to convert to Even in a way that won't break Num
>>> polymorphic functions. If you have any ideas on how to tackle this, I'm all
>>> open to hearing them!
>>>
>>> I agree with you that this is ugly, but I console myself with the thought
>>> that being able to check all monomorphic literals is already a drastic
>>> improvement over the current state. And in the case of lists and strings we
>>> could actually ensure that things work well, since almost no one writes
>>> "IsString polymorphic" code.
>>>
>>> Cheers,
>>> Merijn
>>>
>>> > On 6 Feb 2015, at 16:59, Ryan Trinkle <[hidden email]> wrote:
>>> >
>>> > I think the idea of compile-time validation for overloaded literals is
>>> > fantastic, and doing it with nicer syntax than quasiquoting would really
>>> > improve things.  However, I'm a bit confused about specifically how the
>>> > requirement that it be monomorphic will play into this.  For example, if I
>>> > have:
>>> >
>>> > x = 1
>>> >
>>> > Presumably this will compile, and give a run-time error if I ever
>>> > instantiate its type to Even.  However, if I have:
>>> >
>>> > x :: Even
>>> > x = 1
>>> >
>>> > it will fail to compile?  Furthermore, if I have the former, and type
>>> > inference determines that its type is Even, it sounds like that will also
>>> > fail to compile, but if type inference determines that its type is forall a.
>>> > Nat a => a, then it will successfully compile and then fail at runtime.
>>> >
>>> > Am I understanding this correctly?
>>> >
>>> >
>>> > Ryan
>>> >
>>> > On Fri, Feb 6, 2015 at 8:55 AM, Erik Hesselink <[hidden email]>
>>> > wrote:
>>> > On Fri, Feb 6, 2015 at 2:49 PM, Dominique Devriese
>>> > <[hidden email]> wrote:
>>> > > Agreed.  For the idea to scale, good support for type-level
>>> > > programming with Integers/Strings/... is essential.  Something else
>>> > > that would be useful is an unsatisfiable primitive constraint
>>> > > constructor `UnsatisfiableConstraint :: String -> Constraint` that
>>> > > can
>>> > > be used to generate custom error messages. Then one could write
>>> > > something like
>>> > >
>>> > >   type family MustBeTrue (t :: Bool) (error :: String) :: Constraint
>>> > >   type family MustBeTrue True _ = ()
>>> > >   type family MustBeTrue False error = UnsatisfiableConstraint error
>>> > >
>>> > >   type family MustBeEven (n :: Nat) :: Constraint
>>> > >   type family MustBeEven n = MustBeTrue (IsEven n) ("Error in Even
>>> > > literal :'" ++ show n ++ "' is not even!")
>>> > >
>>> > >   instance (KnownNat n, MustBeEven n) => HasIntegerLiteral Even n
>>> > > where ...
>>> >
>>> > Note that there is a trick to fake this with current GHC: you can
>>> > write an equality constraint that is false, involving the type level
>>> > string:
>>> >
>>> > >   type family MustBeTrue False error = (() ~ error)
>>> >
>>> > Erik
>>> > _______________________________________________
>>> > Glasgow-haskell-users mailing list
>>> > [hidden email]
>>> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>
>>> _______________________________________________
>>> Glasgow-haskell-users mailing list
>>> [hidden email]
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>
>>
>>
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Merijn Verstraaten
In reply to this post by Adam Gundry-2
Hi Adam,

> On 6 Feb 2015, at 21:31, Adam Gundry <[hidden email]> wrote:
> What does "all monomorphic cases" mean? Is the idea what GHC
> would typecheck an expression involving a literal integer, determine
> that the occurrence had type Even, then evaluate the TH splice *after*
> typechecking? Whereas if the occurrence had a non-ground type, it would
> do something else?

Yes, Typed TH already runs *after* type checking, which is what allows you to do validation based on the resulting type. The main reason why I was only proposing to do this for monomorphic values is, because, how could you possible validate a polymorphic literal? Which validation function would you use?

You could ban polymorphic literals, but that'd involve eliminating most uses of polymorphic Num functions (as I mentioned as another email), which would break so much code it would render the extension unusable in "real" code. I'm open to better ideas on how to tackle this, the main reason I started this discussion is because I don't really like this "polymorphic literals fail at compile time" thing either. I just don't see how to solve it without going all dependent types on the problem.

> None of this is particularly persuasive, I'm afraid. Is it worthwhile
> introducing something new just to avoid having to write a quasi quote?

Actually, I would be mildly ok with quasi quoters, BUT there currently is no Typed TH quasi quoter (as mentioned on the wiki page), additionally, such a quoter does not have access to Lift instances for all but a handful of datatypes until we have a more comprehensive way to generate Lift instances. I think both of these points are also highly relevant for this dicussion.

> I *am* attracted to the idea of indexed classes in place of IsString/Num
>
>  class KnownSymbol s => IsIndexedString (a :: *) (s :: Symbol) where
>    fromIndexedString :: a
>
>  class KnownInteger i => IsIndexedInteger (a :: *) (i :: Integer) where
>     fromIndexedInteger :: a
> These have a smooth upgrade path from the existing class instances via
>
>    default fromIndexedString :: (KnownSymbol s, IsString a) => a
>    fromIndexedString = fromString (symbolVal (Proxy :: Proxy s))
>
>    default fromIndexedInteger :: (KnownInteger i, Num a) => a
>    fromIndexedInteger = fromInteger (integerVal (Proxy :: Proxy i))
>
> and other instances can take advantage of the additional type
> information. perhaps we need to bring Dependent Haskell a bit closer
> before this is justifiable...
The main reason I don't like the "dependent haskell" approach or your approach is how much boiler plate it introduces for beginners. ANYONE knows how to write a "String -> Maybe a" function, I barely know how to use your example and I'm very comfortable with the type families/datakinds stuff, how would "ordinary haskellers" use that?

Not to mention, how would I use your "IsIndexedString" in real code? It seems you'd need at least a FunDep + cumbersome annotation? Not to mention that it still performs the conversion at runtime (I would *much* rather have a Lift based approach that just splices finished conversions into the resulting program.

Cheers,
Merijn

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

signature.asc (859 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Adam Gundry-2
Hi Merijn,

Thanks for persevering with explaining things to me. :-)


On 09/02/15 09:47, Merijn Verstraaten wrote:

>> On 6 Feb 2015, at 21:31, Adam Gundry <[hidden email]> wrote:
>> What does "all monomorphic cases" mean? Is the idea what GHC would
>> typecheck an expression involving a literal integer, determine that
>> the occurrence had type Even, then evaluate the TH splice *after*
>> typechecking? Whereas if the occurrence had a non-ground type, it
>> would do something else?
>
> Yes, Typed TH already runs *after* type checking, which is what
> allows you to do validation based on the resulting type. The main
> reason why I was only proposing to do this for monomorphic values is,
> because, how could you possible validate a polymorphic literal? Which
> validation function would you use?
>
> You could ban polymorphic literals, but that'd involve eliminating
> most uses of polymorphic Num functions (as I mentioned as another
> email), which would break so much code it would render the extension
> unusable in "real" code. I'm open to better ideas on how to tackle
> this, the main reason I started this discussion is because I don't
> really like this "polymorphic literals fail at compile time" thing
> either. I just don't see how to solve it without going all dependent
> types on the problem.

In the absence of a coherent story for polymorphism, I think the right
thing to do is to be able to specify a particular validator, rather than
try to have type inference determine a monomorphic type and otherwise
get stuck...


>> None of this is particularly persuasive, I'm afraid. Is it
>> worthwhile introducing something new just to avoid having to write
>> a quasi quote?
>
> Actually, I would be mildly ok with quasi quoters, BUT there
> currently is no Typed TH quasi quoter (as mentioned on the wiki
> page), additionally, such a quoter does not have access to Lift
> instances for all but a handful of datatypes until we have a more
> comprehensive way to generate Lift instances. I think both of these
> points are also highly relevant for this dicussion.

...so is the right solution to introduce Typed TH quasiquoters for
expressions? Sorry, I presumed such a thing existed, as Typed TH is
rather regrettably underdocumented. Is there any particular difficulty
with them, or is it just a Small Matter of Programming?

I think the lack of Lift instances is a separate problem; while it looks
like 7.10 will be better in this respect and dataToExpQ goes a fair way,
I agree that making them easier to generate would be nice. Perhaps a
generics-based default method combined with DeriveAnyClass would make
"deriving Lift" possible?

Adam

--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Merijn Verstraaten
Hi Adam,

> On 9 Feb 2015, at 17:44, Adam Gundry <[hidden email]> wrote:
> In the absence of a coherent story for polymorphism, I think the right
> thing to do is to be able to specify a particular validator, rather than
> try to have type inference determine a monomorphic type and otherwise
> get stuck...

I was planning to write a TH library for this sort of thing anyway, I was just curious if people had better solutions for the polymorphic story/solutions to take away this annoyance. But maybe a better solution in this direction is Gershom's solution to allow proper compile time functions.

> ...so is the right solution to introduce Typed TH quasiquoters for
> expressions? Sorry, I presumed such a thing existed, as Typed TH is
> rather regrettably underdocumented. Is there any particular difficulty
> with them, or is it just a Small Matter of Programming?

I don't actually know the answer to this, it was one of the questions I was hoping to answer in this discussion :)

> I think the lack of Lift instances is a separate problem; while it looks
> like 7.10 will be better in this respect and dataToExpQ goes a fair way,
> I agree that making them easier to generate would be nice. Perhaps a
> generics-based default method combined with DeriveAnyClass would make
> "deriving Lift" possible?

It's not directly related to whatever solution we pick, but I do think it's an important issue. There's currently a TH library for deriving them, but from what I've seen about writing them by hand I don't understand how GHC couldn't trivially generate them for most (all?) ADTs.

Cheers,
Merijn

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

signature.asc (859 bytes) Download Attachment