constraint inference

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

constraint inference

Dmitry Olshansky
Hello, cafe!

If we have many constraints then compiling is sometimes too slow. Especially if there are some type calculations.
And I don't know how to divide this time among different source files because all constraints are checked only when we call a function.

I tried to add constraint info into argument definition instead of the function signature but this trick is not working (see below).

Is it (at least theoretically) possible to infer the constraint inside a function from the type of function's argument?

------------------------------------
$ stack ghci
 ---- GHCi, version 8.0.2: 
Prelude> import Data.Proxy
Prelude Data.Proxy> import GHC.TypeLits
Prelude Data.Proxy GHC.TypeLits> :set -XRankNTypes
Prelude Data.Proxy GHC.TypeLits> let { f :: (KnownSymbol n => Proxy n) -> String; f = symbolVal }

<interactive>:4:54: error:
    • No instance for (KnownSymbol n) arising from a use of ‘symbolVal’
      Possible fix:
        add (KnownSymbol n) to the context of
          the type signature for:
            f :: (KnownSymbol n => Proxy n) -> String
    • In the expression: symbolVal
      In an equation for ‘f’: f = symbolVal
------------------------------------

Best regards,
Dmitry


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: constraint inference

Ivan Lazar Miljenovic
You've specified RankNTypes but aren't using it; did you mean "(forall
n. KnownSymbol n => Proxy n)" ?

Typically in these situations you also can't partially apply it, so
you might need to make it "f p = symbolVal p".

On 7 July 2017 at 15:50, Dmitry Olshansky <[hidden email]> wrote:

> Hello, cafe!
>
> If we have many constraints then compiling is sometimes too slow. Especially
> if there are some type calculations.
> And I don't know how to divide this time among different source files
> because all constraints are checked only when we call a function.
>
> I tried to add constraint info into argument definition instead of the
> function signature but this trick is not working (see below).
>
> Is it (at least theoretically) possible to infer the constraint inside a
> function from the type of function's argument?
>
> ------------------------------------
> $ stack ghci
>  ---- GHCi, version 8.0.2:
> Prelude> import Data.Proxy
> Prelude Data.Proxy> import GHC.TypeLits
> Prelude Data.Proxy GHC.TypeLits> :set -XRankNTypes
> Prelude Data.Proxy GHC.TypeLits> let { f :: (KnownSymbol n => Proxy n) ->
> String; f = symbolVal }
>
> <interactive>:4:54: error:
>     • No instance for (KnownSymbol n) arising from a use of ‘symbolVal’
>       Possible fix:
>         add (KnownSymbol n) to the context of
>           the type signature for:
>             f :: (KnownSymbol n => Proxy n) -> String
>     • In the expression: symbolVal
>       In an equation for ‘f’: f = symbolVal
> ------------------------------------
>
> Best regards,
> Dmitry
>
>
> _______________________________________________
> 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.



--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Fwd: constraint inference

Dmitry Olshansky
Sorry, I didn't copy to cafe...

---------- Forwarded message ----------
From: Dmitry Olshansky <[hidden email]>
Date: 2017-07-07 9:24 GMT+03:00
Subject: Re: [Haskell-cafe] constraint inference
To: Ivan Lazar Miljenovic <[hidden email]>


I am not sure why but when I didn't set RankNTypes I got an appropriate error. So I specified it.

But if I write
  let { f :: (forall n. KnownSymbol n => Proxy n) -> String; f p = symbolVal p }
then nothing is changed.




2017-07-07 9:11 GMT+03:00 Ivan Lazar Miljenovic <[hidden email]>:
You've specified RankNTypes but aren't using it; did you mean "(forall
n. KnownSymbol n => Proxy n)" ?

Typically in these situations you also can't partially apply it, so
you might need to make it "f p = symbolVal p".

On 7 July 2017 at 15:50, Dmitry Olshansky <[hidden email]> wrote:
> Hello, cafe!
>
> If we have many constraints then compiling is sometimes too slow. Especially
> if there are some type calculations.
> And I don't know how to divide this time among different source files
> because all constraints are checked only when we call a function.
>
> I tried to add constraint info into argument definition instead of the
> function signature but this trick is not working (see below).
>
> Is it (at least theoretically) possible to infer the constraint inside a
> function from the type of function's argument?
>
> ------------------------------------
> $ stack ghci
>  ---- GHCi, version 8.0.2:
> Prelude> import Data.Proxy
> Prelude Data.Proxy> import GHC.TypeLits
> Prelude Data.Proxy GHC.TypeLits> :set -XRankNTypes
> Prelude Data.Proxy GHC.TypeLits> let { f :: (KnownSymbol n => Proxy n) ->
> String; f = symbolVal }
>
> <interactive>:4:54: error:
>     • No instance for (KnownSymbol n) arising from a use of ‘symbolVal’
>       Possible fix:
>         add (KnownSymbol n) to the context of
>           the type signature for:
>             f :: (KnownSymbol n => Proxy n) -> String
>     • In the expression: symbolVal
>       In an equation for ‘f’: f = symbolVal
> ------------------------------------
>
> Best regards,
> Dmitry
>
>
> _______________________________________________
> 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.



--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com



_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Fwd: constraint inference

Li-yao Xia-2


On 07/07/2017 02:50 AM, Dmitry Olshansky wrote:
> I am not sure why but when I didn't set RankNTypes I got an appropriate
> error. So I specified it.
>
> But if I write
>    let { f :: (forall n. KnownSymbol n => Proxy n) -> String; f p =
> symbolVal p }
> then nothing is changed.
>
>


What would the String (f Proxy) be? (Note that (Proxy :: forall n.
KnownSymbol n => Proxy n) would be a valid argument here.)
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Fwd: constraint inference

Dmitry Olshansky
You are right, thanks!



2017-07-07 22:17 GMT+03:00 Li-yao Xia <[hidden email]>:


On 07/07/2017 02:50 AM, Dmitry Olshansky wrote:
I am not sure why but when I didn't set RankNTypes I got an appropriate
error. So I specified it.

But if I write
   let { f :: (forall n. KnownSymbol n => Proxy n) -> String; f p =
symbolVal p }
then nothing is changed.




What would the String (f Proxy) be? (Note that (Proxy :: forall n. KnownSymbol n => Proxy n) would be a valid argument here.)

_______________________________________________
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.


_______________________________________________
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.
Loading...