Closed type families, apartness, and occurs check
>From the user manual, it sounds like a clause of a closed type family should >be rejected once no subsitution of the type could make it unify with the >clause. If so, it doesn't seem to do an occurs check: type family IsEq a b :: Bool where IsEq a a = True IsEq a b = False > :kind! forall a . IsEq a a forall a . IsEq a a :: Bool = forall (a :: k). 'True > :kind! forall a . IsEq a [a] forall a . IsEq a [a] :: Bool = forall a. IsEq a [a] I came across this while trying to using Generics to find the immediate children of a term - this sort of non-reduction happens while comparing a type like (Term var) with a constructor argument of type var. Brandon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Closed type families, apartness, and occurs check
Hi Brandon, Yes, this is a dark corner of GHC wherein a proper dragon lurks. In your second example, you're suggesting that, for all types `a`, `a` is never equal to `[a]`. The problem is: that's not true! Consider: > type family G x where > G x = [G x] This is a well-formed, although pathological, type family. What should the behavior of `IsEq (G Int) [G Int]` be? The only possible consistent answer is `True`. This is why `IsEq a [a]` correctly does not reduce. For further information, see section 6 of [1] and for a practical example of how this can cause a program error (with open type families) see [2]. [1]: http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms.pdf [2]: https://ghc.haskell.org/trac/ghc/ticket/8162 It is conceivable that some restrictions around UndecidableInstances (short of banning it in a whole program, including all importing modules) can mitigate this problem, but no one I know has gotten to the bottom of it. Richard On Jul 2, 2014, at 4:19 AM, Brandon Moore wrote: > From the user manual, it sounds like a clause of a closed type family should > be rejected once no subsitution of the type could make it unify with the > clause. If so, it doesn't seem to do an occurs check: > > type family IsEq a b :: Bool where > IsEq a a = True > IsEq a b = False > > > :kind! forall a . IsEq a a > forall a . IsEq a a :: Bool > = forall (a :: k). 'True > > :kind! forall a . IsEq a [a] > forall a . IsEq a [a] :: Bool > = forall a. IsEq a [a] > > I came across this while trying to using Generics to find the immediate > children of a term - this sort of non-reduction happens while comparing a > type like (Term var) with a constructor argument of type var. > > Brandon > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Closed type families, apartness, and occurs check
That was the only thing I worried about, but any examples I tried with families like that ended up with infinite type errors. Infinite types are not meant to be supported, which perhaps gives a solution - the other sensible answer is bottom, i.e. a type checker error or perhaps an infinite loop in the compiler. For instantating with a type family to solve an equation that fails the occurs check, the type family has to be able to already reduce (even if there are some variables), so just adopting the policy that type families be fully expanded before the check would seem to prevent IsEq (G a) [G a] from ever evaulating to true. Brandon On Wednesday, July 2, 2014 7:11 AM, Richard Eisenberg wrote: > > >Hi Brandon, > > >Yes, this is a dark corner of GHC wherein a proper dragon lurks. > > >In your second example, you're suggesting that, for all types `a`, `a` is >never equal to `[a]`. The problem is: that's not true! Consider: > > >> type family G x where >> G x = [G x] > > >This is a well-formed, although pathological, type family. What should the >behavior of `IsEq (G Int) [G Int]` be? The only possible consistent answer is >`True`. This is why `IsEq a [a]` correctly does not reduce. > > >For further information, see section 6 of [1] and for a practical example of >how this can cause a program error (with open type families) see [2]. > > >[1]: http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms.pdf >[2]: https://ghc.haskell.org/trac/ghc/ticket/8162 > > >It is conceivable that some restrictions around UndecidableInstances (short of >banning it in a whole program, including all importing modules) can mitigate >this problem, but no one I know has gotten to the bottom of it. > > >Richard > >On Jul 2, 2014, at 4:19 AM, Brandon Moore wrote: > >From the user manual, it sounds like a clause of a closed type family should >be rejected once no subsitution of the type could make it unify with the >clause. If so, it doesn't seem to do an occurs check: >> >> >>type family IsEq a b :: Bool where >> IsEq a a = True >> IsEq a b = False >> >> >> >>> :kind! forall a . IsEq a a >>forall a . IsEq a a :: Bool >>= forall (a :: k). 'True >>> :kind! forall a . IsEq a [a] >>forall a . IsEq a [a] :: Bool >>= forall a. IsEq a [a] >> >> >> >>I came across this while trying to using Generics to find the immediate >>children of a term - this sort of non-reduction happens while comparing a >>type like (Term var) with a constructor argument of type var. >> >> >> >>Brandon >>___ >>Glasgow-haskell-users mailing list >>Glasgow-haskell-users@haskell.org >>http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >> > > >___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Closed type families, apartness, and occurs check
But that would mean that `IsEq (F a) (F a)` (for some irreducible-for-now `F a`) is stuck, even when we're sure that it will eventually become True. Your approach is perhaps right, but it has negative consequences, too. Richard On Jul 2, 2014, at 9:58 AM, Brandon Moore wrote: > That was the only thing I worried about, but any examples I tried with > families like that ended up with infinite type errors. > Infinite types are not meant to be supported, which perhaps gives a solution > - the other sensible answer is bottom, i.e. a type checker error or perhaps > an infinite loop in the compiler. For instantating with a type family to > solve an equation that fails the occurs check, the type family has to be able > to already reduce (even if there are some variables), so just adopting the > policy that type families be fully expanded before the check would seem to > prevent IsEq (G a) [G a] from ever evaulating to true. > > Brandon > > > On Wednesday, July 2, 2014 7:11 AM, Richard Eisenberg > wrote: > > > Hi Brandon, > > Yes, this is a dark corner of GHC wherein a proper dragon lurks. > > In your second example, you're suggesting that, for all types `a`, `a` is > never equal to `[a]`. The problem is: that's not true! Consider: > > > type family G x where > > G x = [G x] > > This is a well-formed, although pathological, type family. What should the > behavior of `IsEq (G Int) [G Int]` be? The only possible consistent answer is > `True`. This is why `IsEq a [a]` correctly does not reduce. > > For further information, see section 6 of [1] and for a practical example of > how this can cause a program error (with open type families) see [2]. > > [1]: http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms.pdf > [2]: https://ghc.haskell.org/trac/ghc/ticket/8162 > > It is conceivable that some restrictions around UndecidableInstances (short > of banning it in a whole program, including all importing modules) can > mitigate this problem, but no one I know has gotten to the bottom of it. > > Richard > > On Jul 2, 2014, at 4:19 AM, Brandon Moore wrote: > >> From the user manual, it sounds like a clause of a closed type family should >> be rejected once no subsitution of the type could make it unify with the >> clause. If so, it doesn't seem to do an occurs check: >> >> type family IsEq a b :: Bool where >> IsEq a a = True >> IsEq a b = False >> >> > :kind! forall a . IsEq a a >> forall a . IsEq a a :: Bool >> = forall (a :: k). 'True >> > :kind! forall a . IsEq a [a] >> forall a . IsEq a [a] :: Bool >> = forall a. IsEq a [a] >> >> I came across this while trying to using Generics to find the immediate >> children of a term - this sort of non-reduction happens while comparing a >> type like (Term var) with a constructor argument of type var. >> >> Brandon >> ___ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
GHCJS now runs Template Haskell on node.js - Any interest in out of process TH for general cross compilation?
hi all, I've added some code [1] [2] to GHCJS to make it run Template Haskell code on node.js, rather than using the GHC linker. GHCJS has supported TH for a long time now, but so far always relied on native (host) code for it. This is the main reason that GHCJS always builds native and JavaScript code for everything (another is that Cabal Setup.hs scripts need to be compiled to some host-runnable form, but that can also be JavaScript if you have node.js) Now besides the compiler having to do twice the work, this has some other disadvantages: - Our JavaScript code has the same dependencies (packages) as native code, which means packages like unix or Win32 show up somewhere, depending on the host environment. This also limits our options in choosing JS-specific packages. - The Template Haskell code runs on the host environment, which might be slightly different from the target, for example in integer size or operating system specific constants. Moreover, building native code made the GHCJS installation procedure more tricky, making end users think about libgmp or libiconv locations, since it basically required the same preparation as building GHC from source. This change will make installing much easier and more reliable (we still have to update the build scripts). How it works is pretty simple: - When any code needs to be run on the target (hscCompileCoreExpr, through the Hooks API new in GHC 7.8), GHCJS starts a node.js process with the thrunner.js [3] script, - GHCJS sends its RTS and the Template Haskell server code [1] to node.js, the script starts a Haskell thread running the server, - for every splice, GHCJS compiles it to JavaScript and links it using its incremental linking functionality. The code for the splice, including dependencies that have not yet been sent to the runner (for earlier splices), is then sent in a RunTH [4] message, - the runner loads and runs the code in the Q monad, can send queries to GHCJS for reification, - the runner sends back the result as a serialized Template Haskell AST (using GHC.Generics for the Binary instances). All Template Haskell functionality is supported, including recent additions for reifying modules and annotations. I still need to clean up and push the patches for the directory and process packages, but after that, the TH code can read/write files, run processes and interact with them and make network connections, all through node.js. Now since this approach is in no way specific to JavaScript, I was wondering if there's any interest in getting this functionality into GHC 7.10 for general cross compilation. The runner would be a native (target) program with dynamic libraries (or object files) being sent over to the target machine (or emulator) for the splices. Thanks to Andras Slemmer from Prezi who helped build the initial proof of concept (without reification) at BudHac. cheers, Luite [1] https://github.com/ghcjs/ghcjs/blob/414eefb2bb8825b3c4c5cddfec4d79a142bc261a/src/Gen2/TH.hs [2] https://github.com/ghcjs/ghcjs-prim/blob/2dffdc2d732b044377037e1d6ebeac2812d4f9a4/GHCJS/Prim/TH/Eval.hs [3] https://github.com/ghcjs/ghcjs/blob/414eefb2bb8825b3c4c5cddfec4d79a142bc261a/lib/etc/thrunner.js [4] https://github.com/ghcjs/ghcjs-prim/blob/2dffdc2d732b044377037e1d6ebeac2812d4f9a4/GHCJS/Prim/TH/Types.hs#L29 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GHCJS now runs Template Haskell on node.js - Any interest in out of process TH for general cross compilation?
wow, this is great work! If theres a clear path to getting the generic tooling into 7.10, i'm all for it :) (and willing to help on concrete mechanical subtasks) On Wed, Jul 2, 2014 at 12:14 PM, Luite Stegeman wrote: > hi all, > > I've added some code [1] [2] to GHCJS to make it run Template Haskell code > on node.js, rather than using the GHC linker. GHCJS has supported TH for a > long time now, but so far always relied on native (host) code for it. This > is the main reason that GHCJS always builds native and JavaScript code for > everything (another is that Cabal Setup.hs scripts need to be compiled to > some host-runnable form, but that can also be JavaScript if you have > node.js) > > Now besides the compiler having to do twice the work, this has some other > disadvantages: > > - Our JavaScript code has the same dependencies (packages) as native code, > which means packages like unix or Win32 show up somewhere, depending on the > host environment. This also limits our options in choosing JS-specific > packages. > - The Template Haskell code runs on the host environment, which might be > slightly different from the target, for example in integer size or > operating system specific constants. > > Moreover, building native code made the GHCJS installation procedure more > tricky, making end users think about libgmp or libiconv locations, since it > basically required the same preparation as building GHC from source. This > change will make installing much easier and more reliable (we still have to > update the build scripts). > > How it works is pretty simple: > > - When any code needs to be run on the target (hscCompileCoreExpr, through > the Hooks API new in GHC 7.8), GHCJS starts a node.js process with the > thrunner.js [3] script, > - GHCJS sends its RTS and the Template Haskell server code [1] to node.js, > the script starts a Haskell thread running the server, > - for every splice, GHCJS compiles it to JavaScript and links it using its > incremental linking functionality. The code for the splice, including > dependencies that have not yet been sent to the runner (for earlier > splices), is then sent in a RunTH [4] message, > - the runner loads and runs the code in the Q monad, can send queries to > GHCJS for reification, > - the runner sends back the result as a serialized Template Haskell AST > (using GHC.Generics for the Binary instances). > > All Template Haskell functionality is supported, including recent > additions for reifying modules and annotations. I still need to clean up > and push the patches for the directory and process packages, but after > that, the TH code can read/write files, run processes and interact with > them and make network connections, all through node.js. > > Now since this approach is in no way specific to JavaScript, I was > wondering if there's any interest in getting this functionality into GHC > 7.10 for general cross compilation. The runner would be a native (target) > program with dynamic libraries (or object files) being sent over to the > target machine (or emulator) for the splices. > > Thanks to Andras Slemmer from Prezi who helped build the initial proof of > concept (without reification) at BudHac. > > cheers, > > Luite > > [1] > https://github.com/ghcjs/ghcjs/blob/414eefb2bb8825b3c4c5cddfec4d79a142bc261a/src/Gen2/TH.hs > [2] > https://github.com/ghcjs/ghcjs-prim/blob/2dffdc2d732b044377037e1d6ebeac2812d4f9a4/GHCJS/Prim/TH/Eval.hs > [3] > https://github.com/ghcjs/ghcjs/blob/414eefb2bb8825b3c4c5cddfec4d79a142bc261a/lib/etc/thrunner.js > [4] > https://github.com/ghcjs/ghcjs-prim/blob/2dffdc2d732b044377037e1d6ebeac2812d4f9a4/GHCJS/Prim/TH/Types.hs#L29 > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GHCJS now runs Template Haskell on node.js - Any interest in out of process TH for general cross compilation?
This would probably be a great boon for those trying to use haskell for Android and IOS right? how might the emulation setup work for those? On Wed, Jul 2, 2014 at 2:20 PM, Carter Schonwald wrote: > wow, this is great work! > > If theres a clear path to getting the generic tooling into 7.10, i'm all > for it :) (and willing to help on concrete mechanical subtasks) > > > On Wed, Jul 2, 2014 at 12:14 PM, Luite Stegeman > wrote: > >> hi all, >> >> I've added some code [1] [2] to GHCJS to make it run Template Haskell >> code on node.js, rather than using the GHC linker. GHCJS has supported TH >> for a long time now, but so far always relied on native (host) code for it. >> This is the main reason that GHCJS always builds native and JavaScript code >> for everything (another is that Cabal Setup.hs scripts need to be compiled >> to some host-runnable form, but that can also be JavaScript if you have >> node.js) >> >> Now besides the compiler having to do twice the work, this has some other >> disadvantages: >> >> - Our JavaScript code has the same dependencies (packages) as native >> code, which means packages like unix or Win32 show up somewhere, depending >> on the host environment. This also limits our options in choosing >> JS-specific packages. >> - The Template Haskell code runs on the host environment, which might be >> slightly different from the target, for example in integer size or >> operating system specific constants. >> >> Moreover, building native code made the GHCJS installation procedure more >> tricky, making end users think about libgmp or libiconv locations, since it >> basically required the same preparation as building GHC from source. This >> change will make installing much easier and more reliable (we still have to >> update the build scripts). >> >> How it works is pretty simple: >> >> - When any code needs to be run on the target (hscCompileCoreExpr, >> through the Hooks API new in GHC 7.8), GHCJS starts a node.js process with >> the thrunner.js [3] script, >> - GHCJS sends its RTS and the Template Haskell server code [1] to >> node.js, the script starts a Haskell thread running the server, >> - for every splice, GHCJS compiles it to JavaScript and links it using >> its incremental linking functionality. The code for the splice, including >> dependencies that have not yet been sent to the runner (for earlier >> splices), is then sent in a RunTH [4] message, >> - the runner loads and runs the code in the Q monad, can send queries to >> GHCJS for reification, >> - the runner sends back the result as a serialized Template Haskell AST >> (using GHC.Generics for the Binary instances). >> >> All Template Haskell functionality is supported, including recent >> additions for reifying modules and annotations. I still need to clean up >> and push the patches for the directory and process packages, but after >> that, the TH code can read/write files, run processes and interact with >> them and make network connections, all through node.js. >> >> Now since this approach is in no way specific to JavaScript, I was >> wondering if there's any interest in getting this functionality into GHC >> 7.10 for general cross compilation. The runner would be a native (target) >> program with dynamic libraries (or object files) being sent over to the >> target machine (or emulator) for the splices. >> >> Thanks to Andras Slemmer from Prezi who helped build the initial proof of >> concept (without reification) at BudHac. >> >> cheers, >> >> Luite >> >> [1] >> https://github.com/ghcjs/ghcjs/blob/414eefb2bb8825b3c4c5cddfec4d79a142bc261a/src/Gen2/TH.hs >> [2] >> https://github.com/ghcjs/ghcjs-prim/blob/2dffdc2d732b044377037e1d6ebeac2812d4f9a4/GHCJS/Prim/TH/Eval.hs >> [3] >> https://github.com/ghcjs/ghcjs/blob/414eefb2bb8825b3c4c5cddfec4d79a142bc261a/lib/etc/thrunner.js >> [4] >> https://github.com/ghcjs/ghcjs-prim/blob/2dffdc2d732b044377037e1d6ebeac2812d4f9a4/GHCJS/Prim/TH/Types.hs#L29 >> >> ___ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >> >> > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
