Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
data EShow = forall a. Show a = EShow a data E t = forall a. E (a-t) a smallPrint_ t = concatMap (\f- f t) [show . foo, show . bar, show . baz] Yeah, I am aware of these solutions, but like Dan says: but first-class existentials are still desirable because introducing a new type for every existential is annoying. It's comparable to having to write a new class for every combination of argument and result types to mimic first class functions in Java (aside from first class functions being more ubiquitous in their usefulness, although perhaps it only appears that way because we don't have easy use of existential types). I've personally always looked at the extra data type or repeated functions as ugly hacks around the fact that GHC doesn't have real existential typing. Since Haskell is otherwise virtually free of ugly hacks (at least at the level I work at, which doesn't require things like unsafePerformIO and unboxed arrays) this has always annoyed me a bit. So I figured that since we now have a working implementation it would be worth a shot to ask if this language wart can be removed from GHC. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
Thomas Davie wrote: I've found user installs don't work at all on OS X, various people in #haskell were rather surprised to discover this, so apparently it's not the default behavior on other platforms. It really rather makes cabal install rather odd – because it doesn't actually install anything you can use without providing extra options! I'm on OS X and I've always used 'cabal install xyz' without any extra options, installing packages in my home directory instead of globally. I've never had any trouble with it yet. Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On Sun, 2009-04-19 at 00:41 +0200, Thomas Davie wrote: Apparently a user install of uuagc and fgl isn't good enough. Fun to know. I've found user installs don't work at all on OS X, various people in #haskell were rather surprised to discover this, so apparently it's not the default behavior on other platforms. Currently, user installs are the default on all platforms except Windows. It really rather makes cabal install rather odd – because it doesn't actually install anything you can use without providing extra options! It should work fine, you'll need to give more details. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On 19 Apr 2009, at 09:52, Duncan Coutts wrote: On Sun, 2009-04-19 at 00:41 +0200, Thomas Davie wrote: Apparently a user install of uuagc and fgl isn't good enough. Fun to know. I've found user installs don't work at all on OS X, various people in #haskell were rather surprised to discover this, so apparently it's not the default behavior on other platforms. Currently, user installs are the default on all platforms except Windows. It really rather makes cabal install rather odd – because it doesn't actually install anything you can use without providing extra options! It should work fine, you'll need to give more details. This has been the result, at least every time I've installed ghc: $ cabal install xyz $ runhaskell Setup.hs configure -- where abc depends on xyz Configuring abc-0.0... Setup.lhs: At least the following dependencies are missing: xyz -any $ sudo cabal install --global xyz $ runhaskell Setup.hs configure Configuring abc-0.0... $ runhaskell Setup.hs build ... Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On Sun, 2009-04-19 at 10:02 +0200, Thomas Davie wrote: It really rather makes cabal install rather odd – because it doesn't actually install anything you can use without providing extra options! It should work fine, you'll need to give more details. This has been the result, at least every time I've installed ghc: $ cabal install xyz So this does a per-user install. $ runhaskell Setup.hs configure -- where abc depends on xyz This does a global install. Global packages cannot depend on user packages. You have two choices: $ cabal configure because the cabal program does --user installs by default or use $ runhaskell Setup.hs configure --user which explicitly does a --user install. The reason for this confusion is because the original runghc Setup interface started with global installs and we can't easily change that default. On the other hand, per-user installs are much more convenient so that's the sensible default for the 'cabal' command line program. Personally I just always use the 'cabal' program and never use the runghc Setup interface. There's almost never any need to use the runghc Setup interface. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On 19 Apr 2009, at 11:10, Duncan Coutts wrote: On Sun, 2009-04-19 at 10:02 +0200, Thomas Davie wrote: It really rather makes cabal install rather odd – because it doesn't actually install anything you can use without providing extra options! It should work fine, you'll need to give more details. This has been the result, at least every time I've installed ghc: $ cabal install xyz So this does a per-user install. $ runhaskell Setup.hs configure -- where abc depends on xyz This does a global install. Global packages cannot depend on user packages. You have two choices: $ cabal configure because the cabal program does --user installs by default or use $ runhaskell Setup.hs configure --user which explicitly does a --user install. The reason for this confusion is because the original runghc Setup interface started with global installs and we can't easily change that default. On the other hand, per-user installs are much more convenient so that's the sensible default for the 'cabal' command line program. I don't understand what makes user installs more convenient. Certainly, my preference would be for global all the time – I expect something that says it's going to install something to install it onto my computer, like any other installation program does. What is it that makes user installs more convenient in this situation? Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
tom.davie: On 19 Apr 2009, at 11:10, Duncan Coutts wrote: On Sun, 2009-04-19 at 10:02 +0200, Thomas Davie wrote: It really rather makes cabal install rather odd – because it doesn't actually install anything you can use without providing extra options! It should work fine, you'll need to give more details. This has been the result, at least every time I've installed ghc: $ cabal install xyz So this does a per-user install. $ runhaskell Setup.hs configure -- where abc depends on xyz This does a global install. Global packages cannot depend on user packages. You have two choices: $ cabal configure because the cabal program does --user installs by default or use $ runhaskell Setup.hs configure --user which explicitly does a --user install. The reason for this confusion is because the original runghc Setup interface started with global installs and we can't easily change that default. On the other hand, per-user installs are much more convenient so that's the sensible default for the 'cabal' command line program. I don't understand what makes user installs more convenient. Certainly, my preference would be for global all the time – I expect something that says it's going to install something to install it onto my computer, like any other installation program does. What is it that makes user installs more convenient in this situation? You don't need 'sudo' access for user installs. This means that 'cabal install' works out of the box on every system, without needing admin/root privs (esp. important for students). -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
I don't understand what makes user installs more convenient. Certainly, my preference would be for global all the time – I expect something that says it's going to install something to install it onto my computer, like any other installation program does. What is it that makes user installs more convenient in this situation? You don't need 'sudo' access for user installs. This means that 'cabal install' works out of the box on every system, without needing admin/root privs (esp. important for students). But students will be used to needing to configure this – in every other installation system out there they need to tell it to install in their user directory. Personally – I find it more convenient to have the install program do what it says it does! Install it! This would save confusion about old tools that do things globally, and not confuse students, because they're all already used to giving extra flags to make install not install things system wide. Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
Am Sonntag 19 April 2009 13:09:17 schrieb Thomas Davie: I don't understand what makes user installs more convenient. Certainly, my preference would be for global all the time I expect something that says it's going to install something to install it onto my computer, like any other installation program does. What is it that makes user installs more convenient in this situation? You don't need 'sudo' access for user installs. This means that 'cabal install' works out of the box on every system, without needing admin/root privs (esp. important for students). But students will be used to needing to configure this in every other installation system out there they need to tell it to install in their user directory. Personally I find it more convenient to have the install program do what it says it does! Install it! But it does install it, only not where you want it. Just for the record, I (no student, my own computer, sole user) prefer user-installs and cabal's default behaviour. Makes it so much easier to get rid of things I don't want anymore without any fear of buggering my system because something depends on it. This would save confusion about old tools that do things globally, and not confuse students, because they're all already used to giving extra flags to make install not install things system wide. Yes, it is bad that the runhaskell Setup interface has a different default. But, as Duncan said, too late to change it now. Bob ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
* Experimental language extensions, some of which have not been implemented before. Does anybody know if there are any plans to incorporate some of these extensions into GHC - specifically the existential typing ? I would love to be able to use existential typing without having to give up the robustness of GHC.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
Bulat Ziganshin wrote: Hello R.A., Sunday, April 19, 2009, 11:46:53 PM, you wrote: Does anybody know if there are any plans to incorporate some of these extensions into GHC - specifically the existential typing ? it is already here, but you should use forall keyword instead odf exists More particularly, enable Rank2Types and then for any type lambda F and for any type Y which does not capture @a@: (x :: exists a. F a) == (x :: forall a. F a) (f :: exists a. (F a - Y)) == (f :: (forall a. F a) - Y) -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On Sunday 19 April 2009 4:56:29 pm wren ng thornton wrote: Bulat Ziganshin wrote: Hello R.A., Sunday, April 19, 2009, 11:46:53 PM, you wrote: Does anybody know if there are any plans to incorporate some of these extensions into GHC - specifically the existential typing ? it is already here, but you should use forall keyword instead odf exists More particularly, enable Rank2Types and then for any type lambda F and for any type Y which does not capture @a@: (x :: exists a. F a) == (x :: forall a. F a) (f :: exists a. (F a - Y)) == (f :: (forall a. F a) - Y) Eh? I don't think this is right, at least not precisely. The first is certainly not correct, because exists a. F a is F A for some hidden A, whereas forall a. F a can be instantiated to any concrete F A. A higher rank encoding of this existential would be: forall r. (forall a. F a - r) - r encoding the existential as its universal eliminator, similar to encoding an inductive type by its corresponding fold. These two are (roughly?) isomorphic, because you can pass the function: f :: forall a. F a - (exists a. F a) f x = x to the eliminator and get back a value with the existential type. What you can do in GHC is create existentially quantified data types, like so: data E f = forall a. E (f a) Then E F is roughly equivalent to (exists a. F a). And you can also make a type: data E f y = forall a. E (f a - y) where E F Y is the same as (exists a. F a - Y). But here you'd find that you can write: from :: (E f y) - ((forall a. f a) - y) from (E f) fa = f fa but not: to :: ((forall a. f a) - y) - (E f y) to f = E (\fa - f fa) so these two are not equivalent, either. Rather: exists a. (F a - Y) ~ forall r. (forall a. (f a - y) - r) - r where we have: from :: E f y - (forall r. (forall a. (f a - y) - r) - r) from (E f) k = k f to :: (forall r. (forall a. (f a - y) - r) - r) - E f y to k = k E Similarly, you can encode universals as higher-rank existential eliminators. Of course, there are some cases where things reduce more nicely, like: (exists a. F a) - Y == forall a. (F a - Y) In any case, despite being able to encode existentials in this way, or use existentially quantified data types, it might be nice to have first-class existential types like UHC. But, I seem to recall this being investigated for GHC in the past, and it was decided that it added too much complexity with the rest of GHC's type system. My information is sketchy and third hand, though, and perhaps things have changed since then. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
If only it were that easy. Sadly, it's not. Let's look at the following example:
data Test = Test { foo :: Int, bar :: Char, baz :: Bool }
smallPrint t = concatMap (\f - show $ f t) [foo, bar, baz]
In this code the list [foo, bar, baz] should have the type [exists a. Show a =
Test - a].
If we explicitly specify the type, replacing the exists with a forall, then GHC
complains about not being able to match Int, Char and Bool against type a.
Forall is not the same as exists and GHC only implements the former.
From: Bulat Ziganshin [bulat.zigans...@gmail.com]
Sent: 19 April 2009 22:07
To: Niemeijer, R.A.
Cc: haskell-cafe@haskell.org
Subject: Re[2]: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) --
first release
Hello R.A.,
Sunday, April 19, 2009, 11:46:53 PM, you wrote:
Does anybody know if there are any plans to incorporate some of
these extensions into GHC - specifically the existential typing ?
it is already here, but you should use forall keyword instead odf
exists
--
Best regards,
Bulat
mailto:bulat.zigans...@gmail.com___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) --first release
|data Test = Test { foo :: Int, bar :: Char, baz :: Bool }
|smallPrint t = concatMap (\f - show $ f t) [foo, bar, baz]
|In this code the list [foo, bar, baz] should have the type [exists a. Show a =
Test - a].
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
data EShow = forall a. Show a = EShow a
smallPrint t = concatMap (\f- case f t of EShow a - show a) [EShow . foo, EShow . bar, EShow .
baz]
data Test = Test { foo :: Int, bar :: Char, baz :: Bool }
Apart from the extra wrapping, this hardcodes the class. So perhaps
you'd prefer something like
data E t = forall a. E (a-t) a
smallPrint' t = concatMap (\f- case f t of E show a - show a) [E show . foo, E show . bar, E show
. baz]
GHC does have existentials (Hugs has them, too, and HBC had them as well?),
but is more conservative about their use than UHC seems to be.
Claus
PS there's also the old standby of applying the functions in the interface
and letting non-strict evaluation taking care of the rest (keeping the
intermediate type implicit, instead of explicitly hidden):
smallPrint_ t = concatMap (\f- f t) [show . foo, show . bar, show . baz]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
Dan Doel wrote: On Sunday 19 April 2009 4:56:29 pm wren ng thornton wrote: Bulat Ziganshin wrote: Hello R.A., Sunday, April 19, 2009, 11:46:53 PM, you wrote: Does anybody know if there are any plans to incorporate some of these extensions into GHC - specifically the existential typing ? it is already here, but you should use forall keyword instead odf exists More particularly, enable Rank2Types and then for any type lambda F and for any type Y which does not capture @a@: (x :: exists a. F a) == (x :: forall a. F a) (f :: exists a. (F a - Y)) == (f :: (forall a. F a) - Y) Eh? I don't think this is right, at least not precisely. The first is certainly not correct, because exists a. F a is F A for some hidden A, whereas forall a. F a can be instantiated to any concrete F A. Yes, however, because consumers (e.g. @f@) demand that their arguments remain polymorphic, anything which reduces the polymorphism of @a@ in @x@ will make it ineligible for being passed to consumers. Maybe not precise, but it works. Another take is to use (x :: forall a. () - F a) and then once you pass () in then the return value is for some @a@. It's easy to see that this is the same as the version above. A higher rank encoding of this existential would be: forall r. (forall a. F a - r) - r encoding the existential as its universal eliminator, similar to encoding an inductive type by its corresponding fold. Exactly. Whether you pass a polymorphic function to an eliminator (as I had), or pass the universal eliminator to an applicator (as you're suggesting) isn't really important, it's just type lifting: (x :: forall a. F a) == (x :: forall r. (forall a. F a - r) - r) (f :: (forall a. F a) - Y) == (f :: ((forall a. F a - Y) - Y) - Y)) The type lifted version is more precise in the sense that it distinguishes polymorphic values from existential values (rather than overloading the sense of polymorphism), but I don't think it's more correct in any deep way. What you can do in GHC is create existentially quantified data types, like so: data E f = forall a. E (f a) Then E F is roughly equivalent to (exists a. F a). But only roughly. E F has extra bottoms which distinguish it from (exists a. F a), which can be of real interest. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On Sunday 19 April 2009 7:11:51 pm wren ng thornton wrote: Yes, however, because consumers (e.g. @f@) demand that their arguments remain polymorphic, anything which reduces the polymorphism of @a@ in @x@ will make it ineligible for being passed to consumers. Maybe not precise, but it works. Another take is to use (x :: forall a. () - F a) and then once you pass () in then the return value is for some @a@. It's easy to see that this is the same as the version above. No, I'm relatively sure this doesn't work. Take, for instance, F a = a for simplicity. Then we can say: i :: Int i = 5 ei :: exists a. a ei = i Because ei's type, exists a. a, means this expression has some unknown type. And certainly, the value i does have some type; it's Int. By contrast, you won't be writing: ei' :: forall a. a ei' = i and similarly: ei'' :: forall a. () - a ei'' () = i is not a correct type, because i is not a value that belongs to every type. However, we can write: ei''' :: forall r. (forall a. a - r) - r ei''' k = k i as well as translations between types like it and the existential: toE :: (forall r. (forall a. a - r) - r) - (exists a. a) toE f = f (\x - x) toU :: (exists a. a) - (forall r. (forall a. a - r) - r) toU e k = k e 'forall' in GHC means universal quantification. It's doesn't work as both universal and existential quantification. The only way it's involved with existential quantification is when you're defining an existential datatype, where: data T = forall a. C ... is used because the type of the constructor: C :: forall a. ... - T is equivalent to the: C :: (exists a. ...) - T you'd get if the syntax were instead: data T = C (exists a. ...) Which is somewhat confusing, but forall is standing for universal quantification even here. Exactly. Whether you pass a polymorphic function to an eliminator (as I had), or pass the universal eliminator to an applicator (as you're suggesting) isn't really important, it's just type lifting: (x :: forall a. F a) == (x :: forall r. (forall a. F a - r) - r) (f :: (forall a. F a) - Y) == (f :: ((forall a. F a - Y) - Y) - Y)) The type lifted version is more precise in the sense that it distinguishes polymorphic values from existential values (rather than overloading the sense of polymorphism), but I don't think it's more correct in any deep way. I don't really understand what you mean by type lifting. But although you might be able to write functions with types similar to what you've listed above (for instance, of course you can write a function: foo :: (forall a. F a) - (forall r. (forall a. F a - r) - r) foo x k = k x simply because this is essentially a function with type (forall a. F a) - (exists a. F a) and you can do that by instantiating the argument to any type, and then hiding it in an existential), this does not mean the types above are isomorphic, which they aren't in general. But only roughly. E F has extra bottoms which distinguish it from (exists a. F a), which can be of real interest. Well, you can get rid of the extra bottom with data E f = forall a. E !(f a) but first-class existentials are still desirable because introducing a new type for every existential is annoying. It's comparable to having to write a new class for every combination of argument and result types to mimic first class functions in Java (aside from first class functions being more ubiquitous in their usefulness, although perhaps it only appears that way because we don't have easy use of existential types). -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On Sun, 2009-04-19 at 20:46 -0400, Dan Doel wrote: On Sunday 19 April 2009 7:11:51 pm wren ng thornton wrote: Yes, however, because consumers (e.g. @f@) demand that their arguments remain polymorphic, anything which reduces the polymorphism of @a@ in @x@ will make it ineligible for being passed to consumers. Maybe not precise, but it works. Another take is to use (x :: forall a. () - F a) and then once you pass () in then the return value is for some @a@. It's easy to see that this is the same as the version above. No, I'm relatively sure this doesn't work. Take, for instance, F a = a for simplicity. Then we can say: i :: Int i = 5 ei :: exists a. a ei = i Because ei's type, exists a. a, means this expression has some unknown type. And certainly, the value i does have some type; it's Int. By contrast, you won't be writing: ei' :: forall a. a ei' = i and similarly: ei'' :: forall a. () - a ei'' () = i is not a correct type, because i is not a value that belongs to every type. However, we can write: ei''' :: forall r. (forall a. a - r) - r ei''' k = k i as well as translations between types like it and the existential: toE :: (forall r. (forall a. a - r) - r) - (exists a. a) toE f = f (\x - x) toU :: (exists a. a) - (forall r. (forall a. a - r) - r) toU e k = k e You can build a framework around this encoding, pack :: f a - (forall a. f a - r) - r pack x f = f x open :: (forall r.(forall a. f a - r) - r) - (forall a. f a - r) - r open package k = package k Unfortunately, pack is mostly useless without impredicativity and lacking type lambdas requires a motley of data types to be made for f. 'forall' in GHC means universal quantification. It's doesn't work as both universal and existential quantification. The only way it's involved with existential quantification is when you're defining an existential datatype, where: data T = forall a. C ... is used because the type of the constructor: C :: forall a. ... - T is equivalent to the: C :: (exists a. ...) - T you'd get if the syntax were instead: data T = C (exists a. ...) Which is somewhat confusing, but forall is standing for universal quantification even here. Exactly. Whether you pass a polymorphic function to an eliminator (as I had), or pass the universal eliminator to an applicator (as you're suggesting) isn't really important, it's just type lifting: (x :: forall a. F a) == (x :: forall r. (forall a. F a - r) - r) (f :: (forall a. F a) - Y) == (f :: ((forall a. F a - Y) - Y) - Y)) The type lifted version is more precise in the sense that it distinguishes polymorphic values from existential values (rather than overloading the sense of polymorphism), but I don't think it's more correct in any deep way. I don't really understand what you mean by type lifting. But although you might be able to write functions with types similar to what you've listed above (for instance, of course you can write a function: foo :: (forall a. F a) - (forall r. (forall a. F a - r) - r) foo x k = k x simply because this is essentially a function with type (forall a. F a) - (exists a. F a) and you can do that by instantiating the argument to any type, and then hiding it in an existential), You can do this by using undefined, but without using undefined what if F a = Void ? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On Sunday 19 April 2009 9:31:27 pm Derek Elkins wrote:
simply because this is essentially a function with type
(forall a. F a) - (exists a. F a)
and you can do that by instantiating the argument to any type, and then
hiding it in an existential),
You can do this by using undefined, but without using undefined what if
F a = Void ?
If it is, then you're giving me a Void, and I'm putting it in a box.
Apparently I've not installed Agda since I installed GHC 6.10.2, but I'd
expect something like the following to work:
data VoidF (t : Set) : Set where
data Unit : Set where
unit : Unit
data ∃ (f : Set - Set) : Set1 where
box : {t : Set} - f t - ∃ f
box-it : (forall t - VoidF t) - ∃ VoidF
box-it void = box (void Unit)
It's just going to be difficult to get a value with type forall t - VoidF t
in the first place.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On Sat, Apr 18, 2009 at 9:03 AM, a...@cs.uu.nl wrote: Utrecht Haskell Compiler -- first release, version 1.0.0 The UHC team is happy to announce the first public release of the Utrecht Haskell Compiler (UHC). UHC supports almost all Haskell98 features plus many experimental extensions. The compiler runs on MacOSX, Windows (cygwin), and various Unix flavors. Features: * Multiple backends, including a bytecode interpreter backend and a GRIN based, full program analysing backend, both via C. * Experimental language extensions, some of which have not been implemented before. * Implementation via attribute grammars and other high-level tools. * Ease of experimentation with language variants, thanks to an aspect-oriented internal organisation. Getting started Download -- UHC is available for download as source distribution via the UHC home page: http://www.cs.uu.nl/wiki/UHC Here you will also find instructions to get started. Status of the implementation Like any university project UHC is very much work in progress. We feel that it is mature and stable enough to offer to the public, but much work still needs to be done; hence we welcome contributions by others. UHC grew out of our Haskell compiler project (called Essential Haskell Compiler, or EHC) over the past 5 years. UHC internally is organised as a combination of separate aspects, which makes UHC very suitable to experiment with; it is relatively easy to build compilers for sublanguages, or to generate related tools such as documentation generators, all from the same code base. Extensions to the language can be described separately, and be switched on or of as need arises. Warning --- Although we think that the compiler is stable enough to compile subtantial Haskell programs, we do not recommend yet to use it for any serious development work in Haskell. We ourselves use the GHC as a development platform! We think however that it provides a great platform for experimenting with language implementations, language extensions, etc. Mailing lists - For UHC users and developers respectively: http://mail.cs.uu.nl/mailman/listinfo/uhc-users http://mail.cs.uu.nl/mailman/listinfo/uhc-developers Bug reporting - Please report bugs at: http://code.google.com/p/uhc/issues/list The UHC Team -- Atze Dijkstra, Department of Information and Computing Sciences. /|\ Utrecht University, PO Box 80089, 3508 TB Utrecht, Netherlands. / | \ Tel.: +31-30-2534118/1454 | WWW : http://www.cs.uu.nl/~atze . /--| \ Fax : +31-30-2513971 | Email: a...@cs.uu.nl / |___\ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe After running ./configure on my Intel Mac (running OS 10.5.6 with GHC 6.10), I try to run make uhc and get the following: $ make uhc src/ruler2/files.mk:34: build/ruler2/files-ag-d-dep.mk: No such file or directory src/ruler2/files.mk:35: build/ruler2/files-ag-s-dep.mk: No such file or directory mkdir -p build/shuffle ; \ --module=CDoc -dr -Psrc/shuffle/ -o build/shuffle/CDoc.hs src/shuffle/CDoc.ag /bin/sh: --module=CDoc: command not found make: Failed to remake makefile `build/ruler2/files-ag-s-dep.mk'. make: Failed to remake makefile `build/ruler2/files-ag-d-dep.mk'. make EHC_VARIANT=`echo install/101/bin/ehc | sed -n -e 's+install/\([0-9_]*\)/bin/ehc.*+\1+p'` ehc-variant src/ruler2/files.mk:34: build/ruler2/files-ag-d-dep.mk: No such file or directory src/ruler2/files.mk:35: build/ruler2/files-ag-s-dep.mk: No such file or directory mkdir -p build/shuffle ; \ --module=CDoc -dr -Psrc/shuffle/ -o build/shuffle/CDoc.hs src/shuffle/CDoc.ag /bin/sh: --module=CDoc: command not found make[1]: Failed to remake makefile `build/ruler2/files-ag-s-dep.mk'. make[1]: Failed to remake makefile `build/ruler2/files-ag-d-dep.mk'. make EHC_VARIANT_RULER_SEL=((101=HS)).(expr.base patexpr.base tyexpr.base decl.base).(e.int e.char e.var e.con e.str p.str) \ ehc-variant-dflt src/ruler2/files.mk:34: build/ruler2/files-ag-d-dep.mk: No such file or directory src/ruler2/files.mk:35: build/ruler2/files-ag-s-dep.mk: No such file or directory mkdir -p build/shuffle ; \ --module=CDoc -dr -Psrc/shuffle/ -o build/shuffle/CDoc.hs src/shuffle/CDoc.ag /bin/sh: --module=CDoc: command not found make[2]: Failed to remake makefile `build/ruler2/files-ag-s-dep.mk'. make[2]: Failed to remake makefile `build/ruler2/files-ag-d-dep.mk'. make[1]: *** [ehc-variant] Error 2 make: *** [install/101/bin/ehc] Error 2 This is fairly bewildering. Am I the only one seeing errors like this? Thanks, Antoine Also: $ make --version GNU Make 3.81 Copyright (C) 2006 Free
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On 18 Apr 2009, at 22:44, Antoine Latter wrote: On Sat, Apr 18, 2009 at 9:03 AM, a...@cs.uu.nl wrote: Utrecht Haskell Compiler -- first release, version 1.0.0 The UHC team is happy to announce the first public release of the Utrecht Haskell Compiler (UHC). UHC supports almost all Haskell98 features plus many experimental extensions. The compiler runs on MacOSX, Windows (cygwin), and various Unix flavors. Features: * Multiple backends, including a bytecode interpreter backend and a GRIN based, full program analysing backend, both via C. * Experimental language extensions, some of which have not been implemented before. * Implementation via attribute grammars and other high-level tools. * Ease of experimentation with language variants, thanks to an aspect-oriented internal organisation. Getting started Download -- UHC is available for download as source distribution via the UHC home page: http://www.cs.uu.nl/wiki/UHC Here you will also find instructions to get started. Status of the implementation Like any university project UHC is very much work in progress. We feel that it is mature and stable enough to offer to the public, but much work still needs to be done; hence we welcome contributions by others. UHC grew out of our Haskell compiler project (called Essential Haskell Compiler, or EHC) over the past 5 years. UHC internally is organised as a combination of separate aspects, which makes UHC very suitable to experiment with; it is relatively easy to build compilers for sublanguages, or to generate related tools such as documentation generators, all from the same code base. Extensions to the language can be described separately, and be switched on or of as need arises. Warning --- Although we think that the compiler is stable enough to compile subtantial Haskell programs, we do not recommend yet to use it for any serious development work in Haskell. We ourselves use the GHC as a development platform! We think however that it provides a great platform for experimenting with language implementations, language extensions, etc. Mailing lists - For UHC users and developers respectively: http://mail.cs.uu.nl/mailman/listinfo/uhc-users http://mail.cs.uu.nl/mailman/listinfo/uhc-developers Bug reporting - Please report bugs at: http://code.google.com/p/uhc/issues/list The UHC Team -- Atze Dijkstra, Department of Information and Computing Sciences. /|\ Utrecht University, PO Box 80089, 3508 TB Utrecht, Netherlands. / | \ Tel.: +31-30-2534118/1454 | WWW : http://www.cs.uu.nl/ ~atze . /--| \ Fax : +31-30-2513971 | Email: a...@cs.uu.nl / | ___\ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe After running ./configure on my Intel Mac (running OS 10.5.6 with GHC 6.10), I try to run make uhc and get the following: $ make uhc src/ruler2/files.mk:34: build/ruler2/files-ag-d-dep.mk: No such file or directory src/ruler2/files.mk:35: build/ruler2/files-ag-s-dep.mk: No such file or directory mkdir -p build/shuffle ; \ --module=CDoc -dr -Psrc/shuffle/ -o build/shuffle/CDoc.hs src/ shuffle/CDoc.ag /bin/sh: --module=CDoc: command not found make: Failed to remake makefile `build/ruler2/files-ag-s-dep.mk'. make: Failed to remake makefile `build/ruler2/files-ag-d-dep.mk'. make EHC_VARIANT=`echo install/101/bin/ehc | sed -n -e 's+install/\([0-9_]*\)/bin/ehc.*+\1+p'` ehc-variant src/ruler2/files.mk:34: build/ruler2/files-ag-d-dep.mk: No such file or directory src/ruler2/files.mk:35: build/ruler2/files-ag-s-dep.mk: No such file or directory mkdir -p build/shuffle ; \ --module=CDoc -dr -Psrc/shuffle/ -o build/shuffle/CDoc.hs src/ shuffle/CDoc.ag /bin/sh: --module=CDoc: command not found make[1]: Failed to remake makefile `build/ruler2/files-ag-s-dep.mk'. make[1]: Failed to remake makefile `build/ruler2/files-ag-d-dep.mk'. make EHC_VARIANT_RULER_SEL=((101=HS)).(expr.base patexpr.base tyexpr.base decl.base).(e.int e.char e.var e.con e.str p.str) \ ehc-variant-dflt src/ruler2/files.mk:34: build/ruler2/files-ag-d-dep.mk: No such file or directory src/ruler2/files.mk:35: build/ruler2/files-ag-s-dep.mk: No such file or directory mkdir -p build/shuffle ; \ --module=CDoc -dr -Psrc/shuffle/ -o build/shuffle/CDoc.hs src/ shuffle/CDoc.ag /bin/sh: --module=CDoc: command not found make[2]: Failed to remake makefile `build/ruler2/files-ag-s-dep.mk'. make[2]: Failed to remake makefile `build/ruler2/files-ag-d-dep.mk'. make[1]: *** [ehc-variant] Error 2 make: *** [install/101/bin/ehc] Error 2 This is fairly bewildering. Am I the only one seeing errors like this? This looks like the same error I got – see bug report 1 in the bug
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On Sat, Apr 18, 2009 at 4:38 PM, Thomas Davie tom.da...@gmail.com wrote: This looks like the same error I got – see bug report 1 in the bug database – the configure script reports that you have uuagc even if you don't – cabal install it, reconfigure, and you should be on your way. Second thing to watch for – it depends on fgl, but this isn't caught by the configure script. Apparently a user install of uuagc and fgl isn't good enough. Fun to know. Antoine ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
On 19 Apr 2009, at 00:31, Antoine Latter wrote: On Sat, Apr 18, 2009 at 4:38 PM, Thomas Davie tom.da...@gmail.com wrote: This looks like the same error I got – see bug report 1 in the bug database – the configure script reports that you have uuagc even if you don't – cabal install it, reconfigure, and you should be on your way. Second thing to watch for – it depends on fgl, but this isn't caught by the configure script. Apparently a user install of uuagc and fgl isn't good enough. Fun to know. I've found user installs don't work at all on OS X, various people in #haskell were rather surprised to discover this, so apparently it's not the default behavior on other platforms. It really rather makes cabal install rather odd – because it doesn't actually install anything you can use without providing extra options! Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Utrecht Haskell Compiler (UHC) -- first release
I've learnt (the hard way) not to trust user installs at all. On Sun, Apr 19, 2009 at 12:41 AM, Thomas Davie tom.da...@gmail.com wrote: On 19 Apr 2009, at 00:31, Antoine Latter wrote: On Sat, Apr 18, 2009 at 4:38 PM, Thomas Davie tom.da...@gmail.com wrote: This looks like the same error I got – see bug report 1 in the bug database – the configure script reports that you have uuagc even if you don't – cabal install it, reconfigure, and you should be on your way. Second thing to watch for – it depends on fgl, but this isn't caught by the configure script. Apparently a user install of uuagc and fgl isn't good enough. Fun to know. I've found user installs don't work at all on OS X, various people in #haskell were rather surprised to discover this, so apparently it's not the default behavior on other platforms. It really rather makes cabal install rather odd – because it doesn't actually install anything you can use without providing extra options! Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
