ghc-mod and FFI
Hi, recently I run into an issue using ghc-mod, as described here: https://github.com/kazu-yamamoto/ghc-mod/issues/75 In summary, ghc-mod fails if the source file contains a `foreign' declaration. I played around a bit, but I have no experience with the GHC API, so any help is appreciated! Thanks, Bernhard ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
On Mon, Sep 17, 2012 at 1:07 AM, Conal Elliott co...@conal.net wrote: Hi Simon, Yes, I could live with (.-), (.+), etc more easily than `arr`, `plus` etc. Better yet would be a LANGUAGE pragma I can add to my libraries to get the old behavior back. What about treating operators as constructs unless they are mentioned in the forall? ~ is constructor foo :: a ~ b ~ is variable foo :: forall a b (~). a ~ b ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Kind Demotion
I see what you're getting at, but the problem is more fundamental than just the lack of a type *. GHC has no notion of equality between kinds other than syntactic identity. If two kinds are other than syntactically identical, they are considered distinct. This fact basically renders your approach doomed to failure. Furthermore, a promoted datatype and the unpromoted datatype are distinct entities with the same names, so you can't just use a variable both at the kind level and the type level (variable ka in your final ConstructedT example). It is not hard to write a Demote type family that computes an unpromoted datatype from its promoted kind, but that type family will interfere with type inference. That's all the bad news. The good news is that some of us are working out how to extend GHC's rich notion of type equality to the kind level, which would also allow intermingling of type- and kind-variables. We're still a little ways out from starting to think about implementing these ideas, but there's a good chance that what you want will be possible in the (not-so-terribly-long-term) future. Richard On Sep 17, 2012, at 12:41 AM, Ashley Yakeley wrote: TypeRep does indeed resemble * as a type. I'm working on a system for reification of types, building on my open-witness package (which is essentially a cleaner, more Haskell-ish alternative to TypeRep). Firstly, there's a witness type to equality of types: data EqualType :: k - k - * where MkEqualType :: EqualType a a Then there's a class for matching witnesses to types: class SimpleWitness (w :: k - *) where matchWitness :: w a - w b - Maybe (EqualType a b) Then I have a type IOWitness that witnesses to types. Through a little Template Haskell magic, one can declare unique values of IOWitness at top level, or just create them in the IO monad. Internally, it's just a wrapper around Integer, but if the integers match, then it must have come from the same creation, which means the types are the same. data IOWitness (a :: k) = ... instance SimpleWitness IOWitness where ... OK. So what I want to do is create a type that's an instance of SimpleWitness that represents types constructed from other types. For instance, [Integer] is constructed from [] and Integer. data T :: k - * where DeclaredT :: forall ka (a :: ka). IOWitness a - T a ConstructedT :: forall kfa ka (f :: ka - kfa) (a :: ka). T f - T a - T (f a) instance SimpleWitness T where matchWitness (DeclaredT io1) (DeclaredT io2) = matchWitness io1 io2 matchWitness (ConstructedT f1 a1) (ConstructedT f2 a2) = do MkEqualType - matchWitness f1 f2 MkEqualType - matchWitness a1 a2 return MkEqualType matchWitness _ _ = Nothing But this doesn't work. This is because when trying to determine whether f1 a1 ~ f2 a1, even though f1 a1 has the same kind as f2 a2, that doesn't mean that a1 and a2 have the same kind. To solve this, I need to include in ConstructedT a witness to ka, the kind of a: ConstructedT :: forall kfa ka (f :: ka - kfa) (a :: ka). IOWitness ka - T f - T a - T (f a) matchWitness (ConstructedT k1 f1 a1) (ConstructedT k2 f2 a2) = do MkEqualType - matchWitness k1 k2 MkEqualType - matchWitness f1 f2 MkEqualType - matchWitness a1 a2 return MkEqualType Sadly, this doesn't work, for two reasons. Firstly, there isn't a type for *, etc. Secondly, GHC isn't smart enough to unify two kinds even though you've given it an explicit witness to their equality. -- Ashley Yakeley On 16/09/12 20:12, Richard Eisenberg wrote: If you squint at it the right way, TypeRep looks like such a type *. I believe José Pedro Magalhães is working on a revision to the definition of TypeRep incorporating kind polymorphism, etc., but the current TypeRep might work for you. Your idea intersects various others I've been thinking about/working on. What's the context/application? Thanks, Richard On Sep 16, 2012, at 7:09 PM, Ashley Yakeley wrote: Now that we have type promotion, where certain types can become kinds, I find myself wanting kind demotion, where kinds are also types. So for instance there would be a '*' type, and all types of kind * would be demoted to values of it. Is that feasible? -- Ashley Yakeley ___ 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
Hello,
I think that it would be a mistake to have two pragmas with incompatible
behaviors: for example, we would not be able to write modules that use
Conal's libraries and, say, the type nats I've been working on.
If the main issue is the notation for arrows, has anoyone played with what
can be done with the current (7.6) system? I just thought of two
variations that seem to provide a decent notation for writing arrow-ish
programs. The second one, in particular, mirrors the arrow notation at the
value level, so perhaps that would be enough?
-Iavor
{-# LANGUAGE TypeOperators, KindSignatures #-}
module Test where
import Control.Category
-- Variant 1: Post-fix annotation
type (a --- b) c = c a b
f :: Category c = (x --- y) c - (y --- z) c - (x --- z) c
f = undefined
-- Variant 2: Arrow notation
type a -- (c :: * - * - *) = c a
type c -- b = c b
infix 2 --
infix 1 --
g :: Category c = (x --c-- y) - (y --c-- z) - (x --c-- z)
g = undefined
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
Hi,
Note that nobody was suggesting two pragmas with incompatible behaviors, only
to have just one symbol reserved to still be able to have type operator
variables.
I do like your suggestion, although --c-- is quite a bit longer than ~.
Sjoerd
On Sep 17, 2012, at 6:28 PM, Iavor Diatchki wrote:
Hello,
I think that it would be a mistake to have two pragmas with incompatible
behaviors: for example, we would not be able to write modules that use
Conal's libraries and, say, the type nats I've been working on.
If the main issue is the notation for arrows, has anoyone played with what
can be done with the current (7.6) system? I just thought of two variations
that seem to provide a decent notation for writing arrow-ish programs. The
second one, in particular, mirrors the arrow notation at the value level, so
perhaps that would be enough?
-Iavor
{-# LANGUAGE TypeOperators, KindSignatures #-}
module Test where
import Control.Category
-- Variant 1: Post-fix annotation
type (a --- b) c = c a b
f :: Category c = (x --- y) c - (y --- z) c - (x --- z) c
f = undefined
-- Variant 2: Arrow notation
type a -- (c :: * - * - *) = c a
type c -- b = c b
infix 2 --
infix 1 --
g :: Category c = (x --c-- y) - (y --c-- z) - (x --c-- z)
g = undefined
___
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: ANNOUNCE: GHC version 7.6.1
On Fri, Sep 7, 2012 at 11:05 AM, Herbert Valerio Riedel h...@gnu.org wrote: Ian Lynagh i...@well-typed.com writes: On Thu, Sep 06, 2012 at 09:42:53AM -0700, Johan Tibell wrote: 2. Could you please push all the packages that were released in GHC 7.6.1 to Hackage as well? I've now uploaded those that we maintain. ...why has bytestring-0.10.0.0 been held back? (afaics, the last couple of versions on Hackage were uploaded by you as well) Just a reminder that we need that bytestring version on Hackage as other compilers have no way of getting hold of it to fulfill a depedency on bytestring = 0.10. -- Johan ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
Iavor: Wow, I really like the --c-- trick at the type level.
Note: we can shorten that somewhat and improve the fixity to associate
correctly, matching the associativity of (-), which fortunately associates
to the right. (associating to the left can be done with a similar trick,
based on the original version of this hack by Chung-Chieh Shan.)
{-# LANGUAGE TypeOperators, PolyKinds #-}
import Control.Category
infixr 0 ~
infixr 0 ~
type (~) a b = b a
type (~) a b = a b
g :: Category c = (x ~c~ y) - (y ~c~ z) - x ~c~ z
g = undefined
Note, this also has the benefit of picking the correct associativity for
~c~. Unlike naively using a locally bound (~) and avoids the headaches
of picking (--) and (---) or something equally hideous when working with
two categories.
class (Category c, Category d) = CFunctor f c d | f c - d, f d - c where
cmap :: (a ~c~ b) - f a ~d~ f b
-Edward
On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher sjo...@w3future.comwrote:
Hi,
Note that nobody was suggesting two pragmas with incompatible behaviors,
only to have just one symbol reserved to still be able to have type
operator variables.
I do like your suggestion, although --c-- is quite a bit longer than ~.
Sjoerd
On Sep 17, 2012, at 6:28 PM, Iavor Diatchki wrote:
Hello,
I think that it would be a mistake to have two pragmas with incompatible
behaviors: for example, we would not be able to write modules that use
Conal's libraries and, say, the type nats I've been working on.
If the main issue is the notation for arrows, has anoyone played with what
can be done with the current (7.6) system? I just thought of two
variations that seem to provide a decent notation for writing arrow-ish
programs. The second one, in particular, mirrors the arrow notation at the
value level, so perhaps that would be enough?
-Iavor
{-# LANGUAGE TypeOperators, KindSignatures #-}
module Test where
import Control.Category
-- Variant 1: Post-fix annotation
type (a --- b) c = c a b
f :: Category c = (x --- y) c - (y --- z) c - (x --- z) c
f = undefined
-- Variant 2: Arrow notation
type a -- (c :: * - * - *) = c a
type c -- b = c b
infix 2 --
infix 1 --
g :: Category c = (x --c-- y) - (y --c-- z) - (x --c-- z)
g = undefined
___
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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher sjo...@w3future.comwrote: Hi, Note that nobody was suggesting two pragmas with incompatible behaviors, only to have just one symbol reserved to still be able to have type operator variables. An issue with reserving a symbol for type operator variables is it doesn't help you today. 7.6.1 is already released. This means that any change in behavior would have to be in 7.6.2 at the earliest. Assuming the bikeshedding could complete and Simon et al. frantically patched the code tomorrow, rushing to release a 7.6.2 before the platform release. Failing that, you'd have a whole release cycle to wait through, probably a platform, before you could go back to your old behavior, and then your code would have some strange gap of GHC version numbers over which it didn't work. Everyone would have to pretend 7.6.1 never happened, or and break anyone's code that was already written for 7.6, so instead of one breaking change, we'd now have two. For instance, I'm already using ~ in 'github.com/ekmett/indexed.git' for natural transformations and I am loving it, and would be sad to lose it to the choice of ~ as a herald, similarly it would make the ~c~ trick more verbose, and ~ is particularly terrible for operators like ~+~. Other herald choices lead to different issues, '.' is slightly better for the other operators, but makes kind of ugly arrows, plus some day i'd _really_ like to be able to use . as a type constructor for functor composition! It is currently reserved at the type level as an almost accidental consequence of the way forall gets parsed today. I really like Iavor's entirely-in-language way of addressing the issue, due in part to it providing even better associativity than the existing approach, and honestly, even if GHC HQ was somehow convinced to set aside an ad hoc herald for type variables, I'd probably start using it in my code. (probably sandwiching between something like :- and : for old GHC compatibility). I really like that I can just call the Category c, and just get ~c~ or something similar as its arrows. This feels more notationally accurate to me. It also has two major benefits compared to any proposal for adding different heralds: 1.) It is compatible with old code, code written with 7.6.1 and I suppose future code, since (:) is such a remarkably awkward choice of herald for the reasons already documented that it seems an unlikely choice. 2.) I can program with it today. I just realized if you don't want to worry about collisions with the type naturals from GHC.TypeLits, and didn't care about pre-7.6 compatibility, you could strip the notation down all the way to cmap :: CFunctor f c d = (x -c y) - f x -d f y This is even shorter than the conventional cmap :: CFunctor f (~) (~~) = (x ~ y) - f x ~~ f y Which turns the but it is longer argument against it on its head. ;) -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
1) kudos to iavor and edward on the slick notation invention! 2) the key point is that ghc 7.6 does not have support for infix type variable notation, and how to encode infix arrow notations nicely subject that design choice, right? i'm likely just being a tad redundant in this conversation, but it never hurts to sanity check :) cheers -Carter On Mon, Sep 17, 2012 at 6:40 PM, Edward Kmett ekm...@gmail.com wrote: On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher sjo...@w3future.comwrote: Hi, Note that nobody was suggesting two pragmas with incompatible behaviors, only to have just one symbol reserved to still be able to have type operator variables. An issue with reserving a symbol for type operator variables is it doesn't help you today. 7.6.1 is already released. This means that any change in behavior would have to be in 7.6.2 at the earliest. Assuming the bikeshedding could complete and Simon et al. frantically patched the code tomorrow, rushing to release a 7.6.2 before the platform release. Failing that, you'd have a whole release cycle to wait through, probably a platform, before you could go back to your old behavior, and then your code would have some strange gap of GHC version numbers over which it didn't work. Everyone would have to pretend 7.6.1 never happened, or and break anyone's code that was already written for 7.6, so instead of one breaking change, we'd now have two. For instance, I'm already using ~ in 'github.com/ekmett/indexed.git' for natural transformations and I am loving it, and would be sad to lose it to the choice of ~ as a herald, similarly it would make the ~c~ trick more verbose, and ~ is particularly terrible for operators like ~+~. Other herald choices lead to different issues, '.' is slightly better for the other operators, but makes kind of ugly arrows, plus some day i'd _really_ like to be able to use . as a type constructor for functor composition! It is currently reserved at the type level as an almost accidental consequence of the way forall gets parsed today. I really like Iavor's entirely-in-language way of addressing the issue, due in part to it providing even better associativity than the existing approach, and honestly, even if GHC HQ was somehow convinced to set aside an ad hoc herald for type variables, I'd probably start using it in my code. (probably sandwiching between something like :- and : for old GHC compatibility). I really like that I can just call the Category c, and just get ~c~ or something similar as its arrows. This feels more notationally accurate to me. It also has two major benefits compared to any proposal for adding different heralds: 1.) It is compatible with old code, code written with 7.6.1 and I suppose future code, since (:) is such a remarkably awkward choice of herald for the reasons already documented that it seems an unlikely choice. 2.) I can program with it today. I just realized if you don't want to worry about collisions with the type naturals from GHC.TypeLits, and didn't care about pre-7.6 compatibility, you could strip the notation down all the way to cmap :: CFunctor f c d = (x -c y) - f x -d f y This is even shorter than the conventional cmap :: CFunctor f (~) (~~) = (x ~ y) - f x ~~ f y Which turns the but it is longer argument against it on its head. ;) -Edward ___ 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: Kind Demotion
My workaround is to wrap types of all kinds as kind *: data WrapType (a :: k) ...or better yet, as its own kind: data WrappedType = forall a. WrapType a Now I can make an apples-to-apples comparison of types of different kinds, e.g. WrapType [] and WrapType Bool. All I need now is a way of applying wrapped types: type family WrapApply (f :: WrappedType) (x :: WrappedType) :: WrappedType type instance WrapApply (WrapType (f :: ka - kfa)) (WrapType (a :: ka)) = WrapType (f a) -- Ashley Yakeley On 17/09/12 06:05, Richard Eisenberg wrote: I see what you're getting at, but the problem is more fundamental than just the lack of a type *. GHC has no notion of equality between kinds other than syntactic identity. If two kinds are other than syntactically identical, they are considered distinct. This fact basically renders your approach doomed to failure. Furthermore, a promoted datatype and the unpromoted datatype are distinct entities with the same names, so you can't just use a variable both at the kind level and the type level (variable ka in your final ConstructedT example). It is not hard to write a Demote type family that computes an unpromoted datatype from its promoted kind, but that type family will interfere with type inference. That's all the bad news. The good news is that some of us are working out how to extend GHC's rich notion of type equality to the kind level, which would also allow intermingling of type- and kind-variables. We're still a little ways out from starting to think about implementing these ideas, but there's a good chance that what you want will be possible in the (not-so-terribly-long-term) future. Richard On Sep 17, 2012, at 12:41 AM, Ashley Yakeley wrote: TypeRep does indeed resemble * as a type. I'm working on a system for reification of types, building on my open-witness package (which is essentially a cleaner, more Haskell-ish alternative to TypeRep). Firstly, there's a witness type to equality of types: data EqualType :: k - k - * where MkEqualType :: EqualType a a Then there's a class for matching witnesses to types: class SimpleWitness (w :: k - *) where matchWitness :: w a - w b - Maybe (EqualType a b) Then I have a type IOWitness that witnesses to types. Through a little Template Haskell magic, one can declare unique values of IOWitness at top level, or just create them in the IO monad. Internally, it's just a wrapper around Integer, but if the integers match, then it must have come from the same creation, which means the types are the same. data IOWitness (a :: k) = ... instance SimpleWitness IOWitness where ... OK. So what I want to do is create a type that's an instance of SimpleWitness that represents types constructed from other types. For instance, [Integer] is constructed from [] and Integer. data T :: k - * where DeclaredT :: forall ka (a :: ka). IOWitness a - T a ConstructedT :: forall kfa ka (f :: ka - kfa) (a :: ka). T f - T a - T (f a) instance SimpleWitness T where matchWitness (DeclaredT io1) (DeclaredT io2) = matchWitness io1 io2 matchWitness (ConstructedT f1 a1) (ConstructedT f2 a2) = do MkEqualType - matchWitness f1 f2 MkEqualType - matchWitness a1 a2 return MkEqualType matchWitness _ _ = Nothing But this doesn't work. This is because when trying to determine whether f1 a1 ~ f2 a1, even though f1 a1 has the same kind as f2 a2, that doesn't mean that a1 and a2 have the same kind. To solve this, I need to include in ConstructedT a witness to ka, the kind of a: ConstructedT :: forall kfa ka (f :: ka - kfa) (a :: ka). IOWitness ka - T f - T a - T (f a) matchWitness (ConstructedT k1 f1 a1) (ConstructedT k2 f2 a2) = do MkEqualType - matchWitness k1 k2 MkEqualType - matchWitness f1 f2 MkEqualType - matchWitness a1 a2 return MkEqualType Sadly, this doesn't work, for two reasons. Firstly, there isn't a type for *, etc. Secondly, GHC isn't smart enough to unify two kinds even though you've given it an explicit witness to their equality. -- Ashley Yakeley On 16/09/12 20:12, Richard Eisenberg wrote: If you squint at it the right way, TypeRep looks like such a type *. I believe José Pedro Magalhães is working on a revision to the definition of TypeRep incorporating kind polymorphism, etc., but the current TypeRep might work for you. Your idea intersects various others I've been thinking about/working on. What's the context/application? Thanks, Richard On Sep 16, 2012, at 7:09 PM, Ashley Yakeley wrote: Now that we have type promotion, where certain types can become kinds, I find myself wanting kind demotion, where kinds are also types. So for instance there would be a '*' type, and all types of kind * would be demoted to values of it. Is that feasible? -- Ashley Yakeley ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org
