Re: Why cannot inferred type signatures restrict (potentially) ambiguous type variables?
An observation: on GHC 7.6.3, if I remove c2 entirely, then ghci cooperates.
*Main :t \x - c (c x)
\x - c (c x) :: (C a b, C a1 a) = a1 - b
At first blush, I also expected the definition
-- no signature, no ascriptions
c2 x = c (c x)
to type-check. Perhaps GHC adopted a trade-off giving helpful error
messages at the cost of conveniently supporting the local type
refinements like the one Adam used in his instance of C?
On Sat, Oct 12, 2013 at 4:34 PM, adam vogt vogt.a...@gmail.com wrote:
Hello,
I have code:
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses,
ScopedTypeVariables, TypeFamilies #-}
class C a b where c :: a - b
instance (int ~ Integer) = C Integer int where c = (+1)
c2 :: forall a b c. (C a b, C b c) = a - c
c2 x = c (c x :: b)
c2 x = c ((c :: a - b) x)
Why are the type signatures needed? If I leave all of them off, I get:
Could not deduce (C a1 a0)
arising from the ambiguity check for 'c2'
from the context (C a b, C a1 a)
bound by the inferred type for 'c2': (C a b, C a1 a) = a1 - b
from the line: c2 x = c (c x)
From my perspective, it seems that the type signature ghc infers
should be able to restrict the ambiguous types as the hand-written
signature does.
These concerns apply to HEAD (using -XAllowAmbiguousTypes) and ghc-7.6 too.
Regards,
Adam
___
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: TypeHoles behaviour
I also say +1, but I am concerned about always showing all the bindings. In my experiences over the years, the times when holes seem they would have been most helpful is when the bindings were numerous and had large and complicated types. Dumping all of the bindings in that sort of scenario would generate a lot of output to sift through. (Admittedly, I was doing my best Oleg impersonation at the time -- ie complicated type-level programming -- so this is probably relatively uncommon.) I think I nice solution would be a line or two at the top of the message indicating which of the following bindings are most likely relevant? I don't know how intended the current behavior was, but perhaps it could be distilled into a heuristic to guess those relevant bindings. On Tue, Aug 27, 2013 at 10:24 AM, Krzysztof Gogolewski krz.gogolew...@gmail.com wrote: I have also seen this behaviour and support the change. -KG 2013/8/27 Austin Seipp ase...@pobox.com I'm +1 on changing the behavior. I find it probably the most confusing aspect of using TypeHoles, which is otherwise great. On Tue, Aug 27, 2013 at 3:17 AM, Simon Peyton-Jones simo...@microsoft.com wrote: I'm sympathetic to Andres's point here. Easy to implement. Any objections? Simon | -Original Message- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- | boun...@haskell.org] On Behalf Of Andres Löh | Sent: 23 August 2013 21:02 | To: glasgow-haskell-users@haskell.org | Subject: TypeHoles behaviour | | Hi. | | I've just started playing with TypeHoles. (I'm writing some Haskell | course | materials and would like to use them from the very beginning once they | become | available.) | | However, I must say that I don't understand the current notion of | relevance | that seems to determine whether local bindings are included or not. | | The current rule seems to be that bindings are included only if the | intersection between the type variables their types involve and the type | variables in the whole is non-empty. However, I think this is confusing. | | Let's look at a number of examples: | | f1 :: Int - Int - Int | f1 x y = _ | | Found hole '_' with type: Int | In the expression: _ | In an equation for 'f1': f1 x y = _ | | No bindings are shown. | | f2 :: a - a - a | f2 x y = _ | | Found hole '_' with type: a | Where: 'a' is a rigid type variable bound by |the type signature for f2 :: a - a - a at List.hs:6:7 | Relevant bindings include | f2 :: a - a - a (bound at List.hs:7:1) | x :: a (bound at List.hs:7:4) | y :: a (bound at List.hs:7:6) | In the expression: _ | In an equation for 'f2': f2 x y = _ | | Both x and y (and f2) are shown. Why should this be treated differently | from f1? | | f3 :: Int - (Int - a) - a | f3 x y = _ | | Found hole '_' with type: a | Where: 'a' is a rigid type variable bound by |the type signature for f3 :: Int - (Int - a) - a at | List.hs:9:7 | Relevant bindings include | f3 :: Int - (Int - a) - a (bound at List.hs:10:1) | y :: Int - a (bound at List.hs:10:6) | In the expression: _ | In an equation for 'f3': f3 x y = _ | | Here, y is shown, but x isn't, even though y has to be applied to an Int | in order to produce an a. Of course, it's possible to obtain an Int from | elsewhere ... | | f4 :: a - (a - b) - b | f4 x y = _ | | Found hole '_' with type: b | Where: 'b' is a rigid type variable bound by |the type signature for f4 :: a - (a - b) - b at | List.hs:12:7 | Relevant bindings include | f4 :: a - (a - b) - b (bound at List.hs:13:1) | y :: a - b (bound at List.hs:13:6) | In the expression: _ | In an equation for 'f4': f4 x y = _ | | Again, only y is shown, and x isn't. But here, the only sane way of | filling | the hole is by applying y to x. Why is one more relevant than the | other? | | f5 x y = _ | | Found hole '_' with type: t2 | Where: 't2' is a rigid type variable bound by | the inferred type of f5 :: t - t1 - t2 at List.hs:15:1 | Relevant bindings include | f5 :: t - t1 - t2 (bound at List.hs:15:1) | In the expression: _ | In an equation for 'f5': f5 x y = _ | | Neither x and y are included without a type signature. Even though all | of | the above types are admissible, which would convince GHC that one or | even | all may be relevant. | | IMHO, this isn't worth it. It's a confusing rule. Just include all local | bindings | in the output, always. That's potentially verbose, but easy to | understand. It's | also potentially really helpful, because it trains beginning programmers | to see | what types local variables get, and it's a way to obtain complex types |
Re: Marking type constructor arguments as nominal (e.g. Set)
Is the non-injectivity not an issue here because the type family application gets immediately simplified? On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner m...@joachim-breitner.de wrote: Hi, now that roles are in HEAD, I could play around a bit with it. They were introduced to solve the unsoundness of newtype deriving, but there is also the problem of abstraction: If I define a set type based on an ord instance, e.g. data Set a = Set a -- RHS here just for demonstration the I don’t want my users to replace a Set Int by a Set (Down Int), even though the latter is a newtype of the former. This can be prevented by forcing the role of a to be Nominal (and not Representational, as it is by default). What I just noticed is that one does not even have to introduce new syntax for it, one can just use: type family NominalArg x type instance (NominalArg x) = x data Set' a = Set' (NominalArg a) and get different roles; here the excerpt from --show-iface (is there an easier way to see role annotations): 5b7b2f7c3883ef0d9fc7934ac56c4805 data Set a@R [..] 8e15d783d58c18b8205191ed3fd87e27 data Set' a@N The type family does not get into the way, e.g. conv (Set a) = Set' a works as usual. (I now also notice that the parser actually supports role annotations... but still a nice, backward-compatible trick here). Greetings, Joachim -- Joachim “nomeata” Breitner m...@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nome...@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nome...@debian.org ___ 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: Marking type constructor arguments as nominal (e.g. Set)
Non-injectivity of type families sometimes hinders type inference. Consider Set' (Set.singleton 'c') Naively, we only know that (Char ~ NominalArg a). Since type families are not necessarily injective, this usually means we cannot determine the type variable `a' from this constraint. However, since the NominalArg instance is parametric in `a', I suspect GHC might successfully infer (Char ~ a) in this case. … A quick ghci test confirms that GHC does infer (Char ~ a) here. I apologize for not just experimenting in the first place, but maybe this email will save someone slightly more time than is required to read it. :P On Sun, Aug 18, 2013 at 3:37 PM, Joachim Breitner m...@joachim-breitner.dewrote: Hi, not sure – where would injectivity be needed? Greetings, Joachim Am Sonntag, den 18.08.2013, 15:00 -0500 schrieb Nicolas Frisby: Is the non-injectivity not an issue here because the type family application gets immediately simplified? On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner m...@joachim-breitner.de wrote: Hi, now that roles are in HEAD, I could play around a bit with it. They were introduced to solve the unsoundness of newtype deriving, but there is also the problem of abstraction: If I define a set type based on an ord instance, e.g. data Set a = Set a -- RHS here just for demonstration the I don’t want my users to replace a Set Int by a Set (Down Int), even though the latter is a newtype of the former. This can be prevented by forcing the role of a to be Nominal (and not Representational, as it is by default). What I just noticed is that one does not even have to introduce new syntax for it, one can just use: type family NominalArg x type instance (NominalArg x) = x data Set' a = Set' (NominalArg a) and get different roles; here the excerpt from --show-iface (is there an easier way to see role annotations): 5b7b2f7c3883ef0d9fc7934ac56c4805 data Set a@R [..] 8e15d783d58c18b8205191ed3fd87e27 data Set' a@N The type family does not get into the way, e.g. conv (Set a) = Set' a works as usual. (I now also notice that the parser actually supports role annotations... but still a nice, backward-compatible trick here). Greetings, Joachim -- Joachim “nomeata” Breitner m...@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nome...@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nome...@debian.org ___ 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 -- Joachim “nomeata” Breitner m...@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nome...@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nome...@debian.org ___ 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: Exposing newtype coercions to Haskell
On Wed, Jul 3, 2013 at 5:33 AM, Joachim Breitner m...@joachim-breitner.dewrote: [snip] strange, why did I miss that? But I can’t get [the GlobalRdrEnv lookup] to work, even looking up an element that I took from the GRE itself returns []: let e' = head (head (occEnvElts env)) putMsgS $ showSDoc dflags (ppr e') putMsgS $ showSDoc dflags (ppr (lookupGRE_RdrName (nameRdrName (gre_name e')) env)) prints: GHC.NT.Type.NT imported from `GHC.NT.Type' at GHC/NT.hs:5:1-18 (and originally defined at GHC/NT/Type.hs:6:6-7) [] Also, trying to construct a RdrName that I can look up fails: let rdrName = mkRdrQual (mkModuleName GHC.NT.Type) (mkTcOcc NT) putMsgS $ showSDoc dflags (ppr (lookupGRE_RdrName rdrName env)) prints also just []. What am I doing wrong? Thanks, Joachim lookupGRE_RdrName looks something up in the environment and then prunes the results via `pickGREs`. I suspect your lookup is succeeding, but all of your results are getting pruned away. pickGREs :: RdrName - [GlobalRdrElt] - [GlobalRdrElt] -- ^ Take a list of GREs which have the right OccName -- Pick those GREs that are suitable for this RdrName -- And for those, keep only only the Provenances that are suitable -- *Only used for Qual and Unqual, not Orig or Exact* Emphasis mine. NB that `nameRdrName` builds a RdrName via the Exact constructor. That's why your first attempt failed (I think). Your second attempt fails for a sneakier reason, something I posted an email about a little while ago (cf invoking front-end phases from within a GHC plugin?). The GlobalRdrEnv is keyed on the getUnique result of an OccName. That unique is derived from the unique of the FastString contained in the OccName. The uniques of FastStrings are allocated linearly via a global variable. Unfortunately, your plugin image and the hosting compiler's image have distinct copies of this global variable, so FastStrings from your plugin do not get the same unique as the similar FastStrings that were used to build the GlobalRdrEnv's keys. Your plugin creates FastStrings when calling things like `mkTcOcc`, for example. Unless we eventually include the FastStrings' global variable in the `CoreMonad.reinitializeGlobals` mechanism, I think the available workaround here is to filter `occEnvElts env` for gre_names where `occNameString` and `occNameSpace` match what you're looking for. Robustness may require also constraining the gre_prov field. Good luck. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Exposing newtype coercions to Haskell
This is an exciting effort! Just a quick reaction to Simon's comments on CoreM. On Tue, Jul 2, 2013 at 9:11 AM, Simon Peyton-Jones simo...@microsoft.comwrote: To your questions: ** **·**To do these kind of things, CoreM will need more reader stuff. In particular: **o **The global TypeEnv **o **The GlobalRdrEnv For my light experimentation, I have recovered these two values from the ModGuts that all plugins receive. Hopefully someone will shout out if there's pitfalls to avoid. * The mg_rdr_env field is of type GlobalRdrEnv. * compiler/main/GHC.hs defines a function compileCore with a local definition that rebuilds a TypeEnv. I extracted this: \guts - HscTypes.typeEnvFromEntities (CoreSyn.bindersOfBinds (mg_binds guts)) (mg_tcs guts) (mg_fam_insts guts) and it has worked so far. HTH and good luck! ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
SpecConstr and GADTs
I suspect I've found a situation where, to a first approximation, I'd like SpecConstr to run more than once. I'm specializing on GADT constructors that contain coercions, so the constructor-specialized functions have RHSs with refined types. In my situation, those refined types enable simplifications/specializations that eventually result in additional calls that would lead to further constructor-specializations if the eventual calls were somehow already manifest. But it seems that the simplification/specialization only happens after the SpecConstr pass, so the resulting usages don't lead to further constructor-specialized functions. Ticket 2642 http://hackage.haskell.org/trac/ghc/ticket/2642 is the only mention I've seen of the SpecConstr pass being repeated. The more I think about my desired behavior of SpecConstr, the more I suspect that a failure to maximally share the constructor-specializations (leading to possible non-termination) might be a concern if the pass were simply repeated in my particular case. Regarding broader impact, I suspect this situation might arise with heavy uses of single types. Is there any known mechanisms to handle this interaction between SpecConstr and GADTs? I'll be able to provide concrete details about my situation in a few weeks, if anyone is interested. Thanks for your time. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Generating random type-level naturals
When wren's email moved this thread to the top of my inbox, I noticed that
I never sent this draft I wrote. It gives some concrete code along the line
of Wren's suggestion.
-
The included code uses a little of this (singleton types) and a little of
that (implicit configurations).
http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf
http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf
As is so often the case with Haskell discussions, I'm not sure if this is
overkill for your actual needs. There might be simpler possible
solutions, but this idea at least matches my rather literal interpretation
of your email.
Also, I apologize if this approach is what you meant by (Or, more or less
equivalently, one can't write dependently typed functions, and trying to
fake it at the type-level leads to the original problem.)
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
module STandIC where
A data type for naturals; I'm assuming you have something like a useful
Arbitrary instance for these.
data Nat = Z | S Nat
The corresponding singleton type.
data Nat1 :: Nat - * where
Z1 :: Nat1 Z
S1 :: Nat1 n - Nat1 (S n)
Reification of a Nat; cf implicit configurations (ie prepose.pdf).
reifyNat :: Nat - (forall n. Nat1 n - a) - a
reifyNat Z k = k Z1
reifyNat (S n) k = reifyNat n $ k . S1
Here's my questionable assumption:
If the code you want to use arbitrary type-level naturals with
works for all type-level naturals, then it should be possible to
wrap it in a function that fits as the second argument to reifyNat.
That may be tricky to do. I'm not sure it's necessarily always possible in
general; hence questionable assumption. But maybe it'll work for you.
HTH. And I apologize if it's overkill; as Pedro was suggesting, there might
be simpler ways.
On Fri, Nov 16, 2012 at 12:52 AM, wren ng thornton w...@freegeek.orgwrote:
On 11/5/12 6:23 PM, Eric M. Pashman wrote:
I've been playing around with the idea of writing a genetic programming
implementation based on the ideas behind HList. Using type-level
programming, it's fairly straighforward to put together a program
representation that's strongly typed, that supports polymorphism, and that
permits only well-typed programs by construction. This has obvious
advantages over vanilla GP implementations. But it's impossible to generate
arbitrary programs in such a representation using standard Haskell.
Imagine that you have an HList-style heterogenous list of arbitrarily
typed Haskell values. It would be nice to be able to pull values from this
collection at random and use them to build up random programs. But that's
not possible because one can't write a function that outputs a value of
arbitrary type. (Or, more or less equivalently, one can't write dependently
typed functions, and trying to fake it at the type-level leads to the
original problem.)
Actually, you can write functions with the necessary dependent types
using an old trick from Chung-chieh Shan and Oleg Kiselyov:
http://www.cs.rutgers.edu/~**ccshan/prepose/prepose.pdfhttp://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf
The first trick is to reify runtime values at the type level, which the
above paper explains how to do, namely: type class hackery.
The second trick is to overcome the issue you raised about not actually
having dependent types in Haskell. The answer to this is also given in the
paper, but I'll cut to the chase. The basic idea is that we just need to be
able to hide our dependent types from the compiler. That is, we can't
define:
reifyInt :: (n::Int) - ...n...
but only because we're not allowed to see that pesky n. And the reason
we're not allowed to see it is that it must be some particular fixed value
only we don't know which one. But, if we can provide a function eliminating
n, and that function works for all n, then it doesn't matter what the
actual value is since we're capable of eliminating all of them:
reifyInt :: Int - (forall n. ReflectNum n = n - a) - a
This is just the standard CPS trick we also use for dealing with
existentials and other pesky types we're not allowed to see. Edward Kmett
has a variation of this theme already on Hackage:
http://hackage.haskell.org/**package/reflectionhttp://hackage.haskell.org/package/reflection
It doesn't include the implementation of type-level numbers, so you'll
want to look at the paper to get an idea about that, but the reflection
package does generalize to non-numeric types as well.
--
Live well,
~wren
__**_
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.**org Glasgow-haskell-users@haskell.org
http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-usershttp://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing
Re: Unexpected ambiguity in a seemingly valid Haskell 2010 program
My GHC 7.6.1 (on a Mac) compiles this code without any warnings or errors. Do you have some other compilation flags in effect? On Fri, Nov 9, 2012 at 11:09 AM, Roman Cheplyaka r...@ro-che.info wrote: For this module module Test where import System.Random data RPS = Rock | Paper | Scissors deriving (Show, Enum) instance Random RPS where random g = let (x, g') = randomR (0, 2) g in (toEnum x, g') randomR = undefined ghc (7.4.1 and 7.6.1) reports an error: rand.hs:9:9: No instance for (Random t0) arising from the ambiguity check for g' The type variable `t0' is ambiguous Possible fix: add a type signature that fixes these type variable(s) Note: there are several potential instances: instance Random RPS -- Defined at rand.hs:7:10 instance Random Bool -- Defined in `System.Random' instance Random Foreign.C.Types.CChar -- Defined in `System.Random' ...plus 34 others When checking that g' has the inferred type `g' Probable cause: the inferred type is ambiguous In the expression: let (x, g') = randomR (0, 2) g in (toEnum x, g') In an equation for `random': random g = let (x, g') = randomR ... g in (toEnum x, g') Failed, modules loaded: none. There should be no ambiguity since 'toEnum' determines the type of x (Int), and that in turn fixes types of 0 and 2. Interestingly, annotating 0 or 2 with the type makes the problem go away. jhc 0.8.0 compiles this module fine. Roman ___ 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: Using DeepSeq for exception ordering
And the important observation is: all of them throw A if interpreted in
ghci or compiled without -O, right?
On Thu, Nov 8, 2012 at 11:24 AM, Albert Y. C. Lai tre...@vex.net wrote:
On 12-11-08 07:12 AM, Simon Hengel wrote:
I was just going to say that I can give at least one counterexample
where this does not hold:
evaluate (('a' : undefined) `deepseq` return () :: IO ())
throwIO exceptionB
But then I realized that here exceptionA is optimized away altogether.
For me this smells like a bug. Is this related to [1]?
[1]
http://hackage.haskell.org/**trac/ghc/ticket/2273http://hackage.haskell.org/trac/ghc/ticket/2273
Interesting. A few more tests (all GHC 7.4.2, linux, x86 32-bit, use ghc
-O to compile):
The following cases throw A:
import Control.DeepSeq
import Control.Exception
main = do
evaluate (('a' : error A) `deepseq` return () :: Maybe ())
throwIO (userError B)
main = do
evaluate (('a' : error A) `deepseq` ())
throwIO (userError B)
main = do
evaluate (('a' : error A) `deepseq` True)
throwIO (userError B)
main = do
x - evaluate (('a' : error A) `deepseq` putStrLn hi)
x
throwIO (userError B)
The following cases throw B:
main = do
evaluate (('a' : error A) `deepseq` return () :: IO ())
throwIO (userError B)
main = do
evaluate (('a' : error A) `deepseq` putStrLn hi)
throwIO (userError B)
main = do
evaluate (('a' : error A) `deepseq` getLine)
throwIO (userError B)
__**_
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.**org Glasgow-haskell-users@haskell.org
http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-usershttp://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 refinement in type families with PolyKinds
I share an observation/workaround below. On Tue, Oct 30, 2012 at 8:49 AM, Andres Löh andres.l...@gmail.com wrote: This one looks strange to me: -- Stripping a type from all its arguments type family Strip (t :: *) :: k I'd be tempted to read this as saying that Strip :: forall k. * - k So the result of Strip would actually have to be kind-polymorphic. I'm surprised that type instance Strip (Maybe a) = Maybe then doesn't trigger an error. In my experience, such kind arguments are treated like family indices, not parameters. If you add a kind annotation, as below, x :: Apply (Strip (Maybe a) :: * - *) (a ': '[]) :=: Maybe a x = Refl then it type checks. I'm not sure if that scales to your general objective, though. Again, this is based on experience, not inspecting GHC or its theory. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Proposal: EPHEMERAL pragma
The question of whether the warnings should come by default or not is
a question of how serious the programmer is when they declare a type
as EPHEMERAL. In Pedro's use cases, I would be very serious about it —
as Ryan said, performance tends to tank otherwise.
### Proposal Extensions
I think a more granular pragma targeting value declarations would also be nice.
{-# EPHEMERAL T #-}
x = …
This would tell GHC that I really don't want any values of type T in x's core.
It might also make sense to have a EPHEMERAL pragma that has a module
as it's scope.
A related and more expressive pragma might be something like:
{-# USES foo 1, bar 2 #-}
x = …
This hypothetical pragma would similarly a) guide GHC's inliner and b)
emit warnings if the programmer's declared expectations (eg that foo
occurs once and bar occurs twice) are not met by x's ultimate RHS in
Core.
Of course, the cost of the USES pragma's expressiveness is that it may
lead to brittle source code. However, if performance is important
enough to be part of your code's specification, then this may generate
legitimate warnings (perhaps even errors, with a sub-pragma!) —
especially in rather mature performance-focused packages.
On Thu, Oct 25, 2012 at 10:00 AM, Axel Simon axel.si...@in.tum.de wrote:
On 25.10.2012, at 16:45, Johan Tibell wrote:
Interesting idea.
On Thu, Oct 25, 2012 at 6:56 AM, José Pedro Magalhães j...@cs.uu.nl
wrote:
3. Emit a warning if the generated core code still contains uses of Rep.
I think this part will be really annoying, as GHC might end up
generating warnings that the programmer can do nothing about (because
some optimization failed to remove Rep).
I think this is exactly the right idea. A compiler should emit errors about
bad typing since type inference is somewhat complete, but should emit
warnings about other incomplete analyses or optimizations.
If you think that this is too noisy, by all means, don't emit these warnings
by default and add a flag that enables them.
my 2p,
Axel
___
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: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
On Wed, Sep 19, 2012 at 1:51 PM, Richard Eisenberg e...@cis.upenn.edu wrote:
As for recovering kind classes and such once Any is made into a type
family: I'm in favor of finding some way to do explicit kind instantiation,
making the Any trick obsolete. I'm happy to leave it to others to decide the
best concrete syntax.
I'll admit I haven't parsed this entire email thread, but I read
enough of it early on that I wanted to avoid Any recently. Returning
to find this quote from Richard, perhaps the trick I came up is the
one you're after.
(Also — what's the general status on this initiative? Has much
happened in about a month?)
The to my trick key is to use the promotion of this data type.
data KindProxy (k :: *) = KindProxy
I needed it in order to define this family, which counts the number of
arguments a kind has.
type family CountArgs (kp :: KindProxy k) :: Nat
type instance CountArgs (kp :: *) = Z
type instance CountArgs (kp :: kD - kR) = S (CountArgs ('KindProxy ::
KindProxy kR))
The proxy is necessary on the RHS of the second instance, in which I
need a type of kind kR, but I wouldn't have any means to build one
(without Any) were CountArgs simply of kind (k - Nat).
This usage is comparable to Richard's usage in the singletons library,
insomuch as I understand from the Haskell 2012 paper.
I'm less familiar with the usage in GHC.TypeLits. At a quick glance, I
believe I'd change SingE like so
class SingE (kparam :: KindProxy k) rep | kparam - rep where
fromSing :: Sing (a :: k) - rep
instance SingE (kparam :: KindProxy Nat) Integer where
fromSing (SNat n) = n
instance SingE (kparam :: KindProxy Symbol) String where
fromSing (SSym s) = s
However, looking through the rest of that module, I see no point where
a proxy is actually required (as it is required in the second case of
CountArgs). Maybe I'm just missing it, or maybe Iavor is just
interested in *enforcing* the fact that the type is not of
consequence?
Along those same lines… Iavor had SingE instances declared for (Any ::
KindProxy Nat) and (Any :: KindProxy Symbol). I'm not sure why he
didn't leave the type polymorphic, as I have. Perhaps it matters for
various uses of SingE? I haven't tried using my code with examples, so
maybe that's where issues would show up. If it were necessary, the
instances could instead be as follows.
instance SingE ('KindProxy :: KindProxy Nat) Integer where
fromSing (SNat n) = n
instance SingE ('KindProxy :: KindProxy Symbol) String where
fromSing (SSym s) = s
Is this the kind of trick you were after, Richard? It might pollute
the code base and interface a bit with KindProxy wrappers, but I've
not found that insurmountable. Hopefully that isn't a show stopper for
you.
HTH
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
On Thu, Oct 11, 2012 at 10:20 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: The to my trick key is to use the promotion of this data type. The key to my trick is to use the promotion of this data type. Wow — I have no idea what happened there. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: seemingly inconsistent behavior for kind-indexed type constraints in GHC 7.6
On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg e...@cis.upenn.edu wrote:
For similar reasons, GHC does not bring the constraints on an instance into
the context when an instance matches. So, even if GHC did select the instance
you want, it would not bring ('[] ~ ps) into the context.
Ah, of course. I was naively letting myself regarding NLong by its
semantics and not by its instances. Silly mistake.
Part of the reason I made that mistake is that NLong is having the
desired effect on my program in other situations (as my second gist
demonstrates). I still need to characterize how that's working for me
there, but I'm sure your clarification here will surely guide me when
doing so. Thank you.
In past situations like this one, I have effected the desired
implication (to the instance context as instead of to the superclass)
via a coercion, which I make into a rank2 method of the class. It's
just rather tricky to express the type of the coercion in this case,
because of the involved Nat. I'm working on it now.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: seemingly inconsistent behavior for kind-indexed type constraints in GHC 7.6
Just in case anyone is following along at home, here's what I'm going with.
type TakeN n ts = TakeNDropM n Z ts
type family TakeNDropM (n :: Nat) (which :: Nat) (ts :: [k]) :: [k]
type instance TakeNDropM Z which ts = '[]
type instance TakeNDropM (S n) which ts = Nth which ts ': TakeNDropM n (S
which) ts
class (ts ~ TakeN n ts) = NLong (n :: Nat) (ts :: [k])
(Turns out the coercion method itself is unnecessary in this case.)
Now I just have to prove it (by using the requisite ~ constraints on
ts) via instances… in the morning. I think this solution will work out
nicely, based on my previous experiences.
It may turn out to be interesting to compare this convention (of
sprinkling NLong constraints everywhere) to the intended behavior of
using a promoted vector GADT for the kind of ts — eg (ts :: Vec n k).
Thanks for the help, Richard and Gábor. To everyone else, sorry for
the noise/HTH in the future.
On Mon, Oct 8, 2012 at 1:52 AM, Nicolas Frisby nicolas.fri...@gmail.com wrote:
On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg e...@cis.upenn.edu wrote:
For similar reasons, GHC does not bring the constraints on an instance into
the context when an instance matches. So, even if GHC did select the
instance you want, it would not bring ('[] ~ ps) into the context.
Ah, of course. I was naively letting myself regarding NLong by its
semantics and not by its instances. Silly mistake.
Part of the reason I made that mistake is that NLong is having the
desired effect on my program in other situations (as my second gist
demonstrates). I still need to characterize how that's working for me
there, but I'm sure your clarification here will surely guide me when
doing so. Thank you.
In past situations like this one, I have effected the desired
implication (to the instance context as instead of to the superclass)
via a coercion, which I make into a rank2 method of the class. It's
just rather tricky to express the type of the coercion in this case,
because of the involved Nat. I'm working on it now.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Constructing TH types
The issue you had with applications of the [] type seems to be more insidious than my last email made it out to be. This expression ( $(return $ ConE (mkName [])) :: $(return $ ConT (mkName []) `AppT` ConT ''Char) ) fails with [] is applied to too many arguments. I'm thinking that the [] in the type is being resolved somehow to the the [] data constructor, not the [] type constructor. This seems specific to []; the following works for tuples, even though the data and type constructor also share a string name. $(return $ ConE (mkName (,)) `AppE` LitE (CharL 'c') `AppE` LitE (CharL 'a')) :: $(return $ ConT (mkName (,)) `AppT` ConT ''Char `AppT` ConT ''Char) I haven't yet narrowed down where the mkName'd string is (inappropriately?) resolved in the GHC source. Eric, special-casing for ArrowT probably avoids this problem for you. The only thing to glean from this email is that you ideally wouldn't need to worry about the special-casing for your current application — I think there's a TH bug at play, though I haven't found an open GHC ticket for it and it may very well still be a known issue. On Sun, Oct 7, 2012 at 10:15 AM, Eric M. Pashman eric.pash...@gmail.com wrote: Nicolas, thanks for the welcome, and thanks for pointing out the additional 'Type' constructors! I'd looked over the available constructors, but apparently not very well. The 'ListT', 'TupleT', 'ArrowT', etc., constructors are precisely what I need to make this work in a straightforward fashion. So I don't actually have a problem making the right 'Name' value, just a problem reading the TH source. Well, that's that. ... Many thanks, Eric My pleasure. However, ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: seemingly inconsistent behavior for kind-indexed type constraints in GHC 7.6
Thanks. I'll have to spend some more time thinking through those, but
here's two quick responses.
1) Richard: I thought that because OverlappingInstances was not
specified (in this module or any others), GHC would commit to the
instance. If this behavior you suspect is the case, has there been a
discussion of a flag that would disable it?
2) I think I should leak some more of the details of my actual
situation; they seem important if people want to attempt work arounds
(thanks Gábor).
As you may have guessed, I'm not actually interested in a list of ()s.
My actual class is as follows.
class NLong (n :: Nat) (ts :: [k])
instance ('[] ~ ps) = NLong Z ps
instance ((t ': pstail) ~ ps, NLong n pstail) = NLong (S n) ps
I just want to require that the list has n many elements, without
restricting those elements. This is why I'm not using fundeps and type
families — I need to be polymorphic in the elements.
Any alternative ideas given this extra specification details?
-
Further context: I suspect that my use case for this machinery would
be supplanted if we could promote GADTs (esp. vectors of a fixed
length).
I'll share further technical details about the context if there's
interest. Thanks again!
On Sat, Oct 6, 2012 at 7:30 AM, Gábor Lehel illiss...@gmail.com wrote:
I made a version using an associated type and that seems to work fine:
https://gist.github.com/3844758
(In fact you probably don't need a class at all and a simple type
family would be enough.)
On Sat, Oct 6, 2012 at 4:25 AM, Richard Eisenberg e...@cis.upenn.edu wrote:
Hi Nick,
Interesting example.
I think GHC is right in rejecting your instance, but perhaps not for the
reasons you expect.
It would be possible to add another instance to NUnits:
instance NUnits Z '[()]
This would require OverlappingInstances, but because of the possibility of
further instances, GHC rightly does not assume that a matching instance is
the only possible matching instance. So, without that assumption, there is
no reason GHC should unify ts with '[].
For similar reasons, GHC does not bring the constraints on an instance into
the context when an instance matches. So, even if GHC did select the
instance you want, it would not bring ('[] ~ ps) into the context.
To me, both of these problems have solutions: introduce a functional
dependency on NUnits, n - ts; and declare the wanted instance to be
instance NUnits Z '[], without the equality constraint. What's interesting
is that doing both of these changes didn't get the instance accepted. This
*might* be a bug in GHC, but I'd love another opinion before filing, because
I'm really not sure.
Another issue at work here is that GHCi, by default, does not enable
PolyKinds, even when it has loaded a file with PolyKinds. The effect of this
is that printing out polymorphic kinds will see all type variables default
to * without :set -XPolyKinds. That may have had a role to play in the
commentary in the file, but I'm not sure.
Thanks for posting!
Richard
On Oct 5, 2012, at 5:49 PM, Nicolas Frisby wrote:
GHC 7.6 is rejecting some programs that I think ought to be well-typed.
Details here https://gist.github.com/3842579
I find this behavior particularly odd because I can get GHC to deduce
the type equalities in some contexts but not in others. In particular,
it does not deduce them inside of type class instances.
Is this a known issue? I'll create a Trac ticket if that's appropriate.
Thanks for your time.
___
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
--
Your ship was destroyed in a monadic eruption.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: seemingly inconsistent behavior for kind-indexed type constraints in GHC 7.6
On Sat, Oct 6, 2012 at 12:46 PM, Gábor Lehel illiss...@gmail.com wrote: What do you use NLong for? I.e. where and how are you taking advantage of the knowledge that the list is N long? OK, some context. I'm experimenting with an augmentation of the generic-deriving generic programming approach. https://github.com/nfrisby/polyvariadic-generic-deriving Regarding the part of the library that doesn't suffer from the issue in my original email in this thread, user code using the library results in more accurate inferred types because of the NLong constraints. These more accurate inferred types ultimately avoid some ambiguous type variable errors in the user's code. This new gist https://gist.github.com/3847097 demonstrates the benefits that I get from NLong; it gives an example of it eliminating an otherwise ambiguous type variable. It also explains the context of the library a bit more. Thanks. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Comments on current TypeHoles implementation
tl;wr Variables and holes should have disparate syntax, so that code
is easy to locally parse.
Simon, your proposal is very crisp from the GHC implementor's
perspective, but I think it might be harmful from the user's
perspective.
My premise is that free variables — which are normally fatal — should
never be conflated with anything else, regardless of the
circumstances. Similarly, I'd like holes to remain a unique notion; I
don't want (as a GHC user) to think of them as a special case of
anything else.
Also, the scoping of variables versus holes — lexical versus global,
if I understand correctly — seem disparate enough to me that reusing
the complicated one for the simpler one seems dangerously clever.
For example, assuming that -XTypeHoles is on, _foo in one context is
a hole and _foo in another context isn't, depending on what's in
scope (eg the _foo record selector).
If variables and holes do end up conflated in this way, then my above
observations boil down to this: we should provide messages that make
it very difficult for the accidental creation of a hole to go
unnoticed.
Is the principal motivation for the reuse of the variable machinery in
the implementation of holes to avoid a separate syntactic form for
named holes?
Thanks for working on this exciting feature!
On Thu, Oct 4, 2012 at 4:40 AM, Simon Peyton-Jones
simo...@microsoft.com wrote:
There is also the small matter, in this example, of distinguishing which `_'
is which. The description works, but you have to think about it. I don't
have an immediate and simple solution to this. Perhaps the addition of
unique labels (e.g. _$1 _$2). But this is not a major problem. It can even
wait until some future development/expansion on TypeHoles.
I have a proposal. Someone has already suggested on
hackage.haskell.org/trac/ghc/ticket/5910 that an un-bound variable behaves
like a hole. Thus, if you say
f x = y
GHC says “Error: y is not in scope”. But (idea) with -XTypeHoles
f x = y
might generate
1. (renamer) Warning: y is not in scope
2. (type) Error: Hole “y” has type
So that’s like a named hole, in effect.
If you say
f x = 4
GHC warns about the unused binding for x. But if you say
f _x = 4
the unused-binding warning is suppressed. So (idea) if you say
f x = _y
maybe we can suppress warning (1). And, voila, named holes.
Moreover if you add –fdefer-type-errors you can keep going and run the
program.
Any comments? This is pretty easy to do.
(I’m unhappy that –XTypeHoles is a language pragma while –fdefer-type-errors
is a compiler flag. Maybe we should have –XDeferTypeErrors?)
Simon
From: sean.leat...@gmail.com [mailto:sean.leat...@gmail.com] On Behalf Of
Sean Leather
Sent: 03 October 2012 16:45
To: Simon Peyton-Jones
Cc: GHC Users List; Thijs Alkemade
Subject: Comments on current TypeHoles implementation
Hi Simon,
Thanks for all your work in getting TypeHoles into HEAD. We really
appreciate it.
I was playing around with HEAD today and wanted to share a few observations.
(1) One of the ideas we had was that a hole `_' would be like `undefined'
but with information about the type and bindings. But in the current
version, there doesn't appear to be that connection. This mainly applies to
ambiguous type variables.
Consider:
f = show _
The hole has type a0.
But with
f = show undefined
there is a type error because a0 is ambiguous.
We were thinking that it would be better to report the ambiguous type
variable first, rather than the hole. In that case, tou can use
-fdefer-type-errors to defer the error. Currently, you don't have that
option. I can see the argument either way, however, and I'm not sure which
is better.
(2) There is a strange case where an error is not reported for a missing
type class instance, even though there is no (apparent) relation between the
missing instance and the hole. (This also relates to the connection to
`undefined', but less directly.)
We have the following declaration:
data T = T Int {- no Show instance -}
With a hole in the field
g = show (T _)
we get a message that the hole has type Int.
With
g = show (T undefined)
we get an error for the missing instance of `Show T'.
(3) In GHCi, I see that the type of the hole now defaults. This is not
necessarily bad, though it's maybe not as useful as it could be.
ghci :t show _
reports that the hole has type ().
(4) In GHCi, sometimes a hole throws an exception, and sometimes it does
not.
ghci show _
throws an exception with the hole warning message
ghci show (T _)
and
ghci _ + 42
cause GHCi to panic.
(5) There are some places where unnecessary parentheses are used when
pretty-printing the code:
ghci :t _ _
interactive:1:1: Warning:
Found hole `_' with type t0 - t
Where: `t0' is a free type variable
`t' is a rigid type variable
Re: Comments on current TypeHoles implementation
On Thu, Oct 4, 2012 at 4:28 PM, Roman Cheplyaka r...@ro-che.info wrote: I don't see why it is an issue. You should never encounter holes in the released code. The only source of holes should be stuff that you just wrote. With this proposal not only you get an error for the unbound variable (as you'd get before), but GHC even tells you the type of a thing that you should plug there! Roman That's a good point. Upon reflection, my concerns are motivated by how I expect I'll be using holes. I anticipate that will be for dealing with complex code, and that's when I really don't want any other surprises. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Problem with default signatures
I've investigated this behavior a bit, and I have two things worth mentioning.
(1) One of the ingredients in this behavior is the non-injectivity
of type families. If we make the class parameter f accessible in the
signature of emptyAlt, there are no more type errors. For example, if
you can change the signature to emptyAlt :: Proxy f - Exp (AltGRep f)
where
data Proxy (f :: * - *) = Proxy
(Even if your code had been type checking, you would have found that
emptyAlt would be impossible to use with the signature you gave it —
its type must include at least one occurrence of each class parameter
that isn't inside an argument to a type family. That's what I mean by
accessible, and its what the dummy parameter Proxy f gives us.)
Jeroen Weijers, I think this will be enough for you to get past these
errors. Please let me know if not.
The rest of this email is probably more for GHC hackers.
(2) The note [Default methods in instances] in TcInstDcls handles
GHC ticket #1061. The key idea is that a default method (those without
special signatures) intuitively results in a method definition in the
instances that rely on the default is a simple equality method =
default_RHS. #1061 shows a situation in which this won't do; we need
the RHS to be eta-expanded with respect to the class type parameters.
But looking in TcInstDcls.tcInstanceMethods and
TcClassDcl.mkGenericDefMethBind, it seems that generic default
signatures don't do this eta-expansion.
Adding the Proxy parameter as in (1) avoids the type errors and also
seems like it's going to be necessary, so I'm not sure (2) is entirely
relevant. But I'm not seeing why generic default methods would be any
different with respect to #1061 than vanilla default methods. Perhaps
the example in #1061 could be enriched with a default signature to see
if its fix should be applied to generic default methods as well?
Lastly, regarding (1), would it make sense to throw an error when a
polymorphic signature has inaccessible type variables? Are these
ever useful? Maybe just a warning?
HTH
On Tue, Aug 21, 2012 at 4:45 AM, Jeroen Weijers jeroenweij...@gmail.com wrote:
Hello,
I am trying to create some code involving type families and default
signatures. I am getting a type error that I do not understand (as far as I
can see the error is wrong).
I removed all code that doesn't contribute to the error:
{-# LANGUAGE DeriveGeneric, UndecidableInstances, DefaultSignatures,
TypeOperators, GADTs, FlexibleContexts, TypeFamilies, FlexibleInstances #-}
module Database.DSH.Problem where
import GHC.Generics
data Exp a where
UnitE :: Exp ()
ListE :: [Exp a] - Exp [Exp a]
class GenericQA f where
type GRep f
type AltGRep f
type AltGRep f = [Exp (GRep f)]
gToExp :: f a - Exp (GRep f)
emptyAlt :: Exp (AltGRep f)
default emptyAlt :: (AltGRep f ~ [Exp (GRep f)]) = Exp (AltGRep f)
emptyAlt = ListE []
instance GenericQA U1 where
type GRep U1 = ()
gToExp U1 = UnitE
This gives me the following type errors:
Problem.hs:19:10:
Couldn't match type `AltGRep f0' with `[Exp ()]'
Expected type: AltGRep U1
Actual type: AltGRep f0
Expected type: Exp (AltGRep U1)
Actual type: Exp (AltGRep f0)
In the expression: (Database.DSH.Problem.$gdmemptyAlt)
In an equation for `emptyAlt':
emptyAlt = (Database.DSH.Problem.$gdmemptyAlt)
Problem.hs:19:10:
Couldn't match type `GRep f0' with `()'
Expected type: [Exp (GRep f0)]
Actual type: AltGRep f0
In the expression: (Database.DSH.Problem.$gdmemptyAlt)
In an equation for `emptyAlt':
emptyAlt = (Database.DSH.Problem.$gdmemptyAlt)
In the instance declaration for `GenericQA U1'
In this error the type variable f0 is mentioned but as far as I understand it
f should have been instantiated to U1 and not to a variable f0. I've tried
many variations on the default type signature for emptyAlt but haven't found
any that doesn't result in this error. Can somebody explain what is going
wrong here?
Cheers,
Jeroen
___
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: Request for comments on proposal for literate programming using markdown
On Wed, Aug 22, 2012 at 10:02 AM, Nicolas Frisby nicolas.fri...@gmail.com wrote: Maybe just try again in a separate thread? Perhaps under a pseudonym! :) Whoa, just realized once again that email is tone-deaf. I meant that 'pseudonym' thing cheekily: just to help differentiate the proposal in a silly way. In no way was it supposed to be insulting! Sorry for the noise. Also, for the record, I would like for markdown to be an option — regardless of other practical considerations at the moment. It might also be attractive to web people as they check out Haskell. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: faking universal quantification in constraints
Thanks! I'll analyze what you've done here. One thing that jumps out at me is that you're using flop twice. I think this violates an invariant that I was trying(/hoping) to maintain by not exporting Skolem. I'll let you know once I look at it longer. Thanks for taking the time to do this. On Tue, Apr 17, 2012 at 1:40 PM, Dimitrios Vytiniotis dimit...@microsoft.com wrote: Hi Nick, I cannot say that I understand very well what you have in your mind, nor the signatures of the classes you have in your module, but as you expected your program is unsafe (and I've probably attached one of the most obfuscated ways to show it, many apologies for this! At least my code can offer a good laugh to people :-)) Because I do not understand what you are doing in this module, I also do not understand how to make it safer -- I just can safely tell you that using your forall_S one can create a Leibniz equality: forall a c. c Skolem - c a which (by a free theorem) means that ALL types must be equal to Skolem, and my code exploits exactly this to equate Char to Skolem to Int - Int. The fact that you can't name Skolem in the new module because it is not exported is kind of irrelevant ... Regarding impredicativity in GHC, we are still unfortunately on the whiteboard ... Hope this helps! d- -Original Message- From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell- users-boun...@haskell.org] On Behalf Of Nicolas Frisby Sent: Monday, April 16, 2012 11:58 PM To: glasgow-haskell-users Subject: faking universal quantification in constraints I'm simulating skolem variables in order to fake universal quantification in constraints via unsafeCoerce. http://hpaste.org/67121 I'm not familiar with various categories of types from the run-time's perspective, but I'd be surprised if there were NOT a way to use this code to create run-time errors. Is there a way to make it safer? Perhaps by making Skolem act more like GHC's Any type? Or perhaps like the - type? I'd like to learn about the varieties of types from the run-time's perspective. I know Dimitrios Vytiniotis is trying to implement these legitimately in GHC, but I don't know much about that project's status, nor any documentation indicating how to try it out in GHC HEAD (e.g. what's the syntax?). Is there a page on the GHC wiki or something to check that sort of thing? I wonder how far this Forall_S trick can take me in the interim towards Vytiniotis' objective functionality when paired with a (totally safe) class for implication. class Implies (ante :: Constraint) (conc :: Constraint) where impliesD :: Dict ante - Dict conc Thanks, Nick ___ 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: faking universal quantification in constraints
In http://hpaste.org/67172, I've simplified your demonstration to define a function uhoh :: forall a b. Dict (a ~ b) Essentially, I had forgot about ~ constraints. The reason I wasn't exporting Skolem was so that if there were a satisfiable constraint (c Skolem), I could infer that the corresponding instances was totally polymorphic in the argument. That's bogus reasoning because of ~ (and hence fundeps, as you used). Thanks again. On Tue, Apr 17, 2012 at 2:14 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: Thanks! I'll analyze what you've done here. One thing that jumps out at me is that you're using flop twice. I think this violates an invariant that I was trying(/hoping) to maintain by not exporting Skolem. I'll let you know once I look at it longer. Thanks for taking the time to do this. On Tue, Apr 17, 2012 at 1:40 PM, Dimitrios Vytiniotis dimit...@microsoft.com wrote: Hi Nick, I cannot say that I understand very well what you have in your mind, nor the signatures of the classes you have in your module, but as you expected your program is unsafe (and I've probably attached one of the most obfuscated ways to show it, many apologies for this! At least my code can offer a good laugh to people :-)) Because I do not understand what you are doing in this module, I also do not understand how to make it safer -- I just can safely tell you that using your forall_S one can create a Leibniz equality: forall a c. c Skolem - c a which (by a free theorem) means that ALL types must be equal to Skolem, and my code exploits exactly this to equate Char to Skolem to Int - Int. The fact that you can't name Skolem in the new module because it is not exported is kind of irrelevant ... Regarding impredicativity in GHC, we are still unfortunately on the whiteboard ... Hope this helps! d- -Original Message- From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell- users-boun...@haskell.org] On Behalf Of Nicolas Frisby Sent: Monday, April 16, 2012 11:58 PM To: glasgow-haskell-users Subject: faking universal quantification in constraints I'm simulating skolem variables in order to fake universal quantification in constraints via unsafeCoerce. http://hpaste.org/67121 I'm not familiar with various categories of types from the run-time's perspective, but I'd be surprised if there were NOT a way to use this code to create run-time errors. Is there a way to make it safer? Perhaps by making Skolem act more like GHC's Any type? Or perhaps like the - type? I'd like to learn about the varieties of types from the run-time's perspective. I know Dimitrios Vytiniotis is trying to implement these legitimately in GHC, but I don't know much about that project's status, nor any documentation indicating how to try it out in GHC HEAD (e.g. what's the syntax?). Is there a page on the GHC wiki or something to check that sort of thing? I wonder how far this Forall_S trick can take me in the interim towards Vytiniotis' objective functionality when paired with a (totally safe) class for implication. class Implies (ante :: Constraint) (conc :: Constraint) where impliesD :: Dict ante - Dict conc Thanks, Nick ___ 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: faking universal quantification in constraints
Great! I'll take a whack at it ;) On Tue, Apr 17, 2012 at 4:07 PM, Edward Kmett ekm...@gmail.com wrote: On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: I'm simulating skolem variables in order to fake universal quantification in constraints via unsafeCoerce. http://hpaste.org/67121 I'm not familiar with various categories of types from the run-time's perspective, but I'd be surprised if there were NOT a way to use this code to create run-time errors. Is there a way to make it safer? Perhaps by making Skolem act more like GHC's Any type? Or perhaps like the - type? I'd like to learn about the varieties of types from the run-time's perspective. FWIW- I have a version of this concept packaged up in the constraints package. I had a small example that abused flexible instances and MPTCs to cause the single Skolem version of my code to fail. However, when I refined it to use two Skolem variables I wasn't able to derive sufficient Oleggery to break it. That said, an absence of a counter-example isn't a proof that it can't exist. http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: faking universal quantification in constraints
I built a (really ugly) dictionary for (Int ~ Char) using Data.Constraints.Forall. I'm fairly confident it could be generalized to a polymorphic coercion (a ~ b). http://hpaste.org/67180 I cheated with overlapping instances, but you left me no choice ;). Anyone who pulls this kind of stunt is definitely trying to subvert it; so I vote trustworthy. I'm adopting Data.Constraints.Forall for my local experimentation. Thanks for pointing it out. On Tue, Apr 17, 2012 at 4:15 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: Great! I'll take a whack at it ;) On Tue, Apr 17, 2012 at 4:07 PM, Edward Kmett ekm...@gmail.com wrote: On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: I'm simulating skolem variables in order to fake universal quantification in constraints via unsafeCoerce. http://hpaste.org/67121 I'm not familiar with various categories of types from the run-time's perspective, but I'd be surprised if there were NOT a way to use this code to create run-time errors. Is there a way to make it safer? Perhaps by making Skolem act more like GHC's Any type? Or perhaps like the - type? I'd like to learn about the varieties of types from the run-time's perspective. FWIW- I have a version of this concept packaged up in the constraints package. I had a small example that abused flexible instances and MPTCs to cause the single Skolem version of my code to fail. However, when I refined it to use two Skolem variables I wasn't able to derive sufficient Oleggery to break it. That said, an absence of a counter-example isn't a proof that it can't exist. http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
faking universal quantification in constraints
I'm simulating skolem variables in order to fake universal quantification in constraints via unsafeCoerce. http://hpaste.org/67121 I'm not familiar with various categories of types from the run-time's perspective, but I'd be surprised if there were NOT a way to use this code to create run-time errors. Is there a way to make it safer? Perhaps by making Skolem act more like GHC's Any type? Or perhaps like the - type? I'd like to learn about the varieties of types from the run-time's perspective. I know Dimitrios Vytiniotis is trying to implement these legitimately in GHC, but I don't know much about that project's status, nor any documentation indicating how to try it out in GHC HEAD (e.g. what's the syntax?). Is there a page on the GHC wiki or something to check that sort of thing? I wonder how far this Forall_S trick can take me in the interim towards Vytiniotis' objective functionality when paired with a (totally safe) class for implication. class Implies (ante :: Constraint) (conc :: Constraint) where impliesD :: Dict ante - Dict conc Thanks, Nick ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: How to declare polymorphic instances for higher-kinded types?
Here's another alternative.
newtype Comp f g a = Comp {unComp :: f (g a)}
instance Resolvable e = Resolvable (Maybe `Comp` e) where
resolve db = fmap Comp . resolveMaybe db . unComp
One disadvantage of this approach is that it requires you to pepper
your types with explicit compositions of *-* types via Comp.
On Mon, Mar 5, 2012 at 3:14 AM, Herbert Valerio Riedel h...@gnu.org wrote:
Fair enough, but trying to workaround this by defining a type-synonym to
get an (*-*)-kinded expression didn't work either, as currying doesn't
seem to be supported at the type-level (is there a language-extension
for that?):
The Comp newtype provides the type-level currying you were after,
which cannot be done with type synonyms. There is no
language-extension for that that I'm aware of. If you want to venture
down that rabbit hole, maybe take a look at Her.
https://personal.cis.strath.ac.uk/~conor/pub/she/
The other disadvantage of this approach is that Comp only works for a
fixed number of arguments. Thus *-*-* types, like pairs, requires Comp2.
newtype Comp2 f g h a = Comp2 {unComp2 :: f (g a) (h a)}
instance (Resolvable e0, Resolvable e1) = Resolvable (Comp2 (,) e0 e1) where
resolve db = fmap Comp2 . resolvePair db . unComp2
So, if you don't mind adding types like Comp, Comp2, etc throughout
the types in your program/library, this let's you keep Resolvable's
parameter as (* - *) and avoids the type families and constraint
kinds.
I personally prefer the implicitness and generality of Löh's approach,
but I also know that some people (perhaps your users) are shy to the
newer type extensions.
HTH
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
packaged up polykinded types can't index type families?
I suspect I'm tripping on a gap in the PolyKinds support. I'm trying
to package up a type-level generic view. It uses PolyKinds — and
DataKinds, but I think it's the PolyKinds that matter. If I compile
everything locally in the same build, it works fine. If I isolate the
spine view declarations in their own package, I get type errors.
A quick search turned up this omnibus, which I'm guessing might fix my problem.
http://hackage.haskell.org/trac/ghc/changeset/3bf54e78cfd4b94756e3f21c00ae187f80c3341d
I was hoping someone might be able to identify if that's the case. I
can wait for 7.6.1 if I must, but I was wondering if there's a
workaround.
(If I avoid PolyKinds, it works. But I have to simulate PolyKinds for
a finite set of kinds, which is pretty obfuscating and not general. If
you're curious, checkout the type-spine package. This whole email
regards my trying to generalize and simplify that package with
PolyKinds.)
In a distillation of my use case, we have two modules. The first is
the type-level spine view.
{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators,
UndecidableInstances, TemplateHaskell, EmptyDataDecls #-}
module Spine where
type family Spine a :: *
data Atom n -- represents a totally unapplied type name
data f :@ a -- |represents a type-level application
-- this is an unsaturated instance, which might be a no-no, but
-- at least isn't obviously causing the current problem
type instance Spine (f a) = f :@ a
-- all other instances are for unapplied types names:
- e.g. type instance Spine N = Atom N
spineType :: Name - Q [Dec]
spineType n = let t = conT n in
(:[]) `fmap` tySynInstD ''Spine [t] [t| Atom $t |]
The second module is a distilled use case.
{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators,
TemplateHaskell #-}
module Test where
import Spine -- our first module above
type family IsApp (a :: *) :: Bool
type instance IsApp (Atom n) = False
type instance IsApp (a :@ b) = True
-- example types and use
data A = A
data F a = F a
concat `fmap` mapM spineType [''A, ''F]
isApp :: (True ~ IsApp (Spine a)) = a - ()
isApp _ = ()
test :: ()
test = isApp (F A)
If Spine.hs and Test.hs are in the same directory and I load Test in
ghci, it type-checks fine. If I instead use cabal to install Spine as
its own package, the subsequent type-checking of Test.test fails with:
Couldn't match type `IsApp ((:@) (* - *) * F A)' with `'True'
The :bro Spine command returns the same information regardless of how
Test imports Spine.
*Test :bro Spine
type family Spine k a :: *
data Atom k n
data (:@) k k f a
spineType :: ...snip...
Why can IsApp (... :@ ...) reduce if Spine was locally compiled but
not if it's pulled from a package? Is there some crucial info that the
package interfaces can't yet express? Is there an open bug for this?
Thanks for your time,
Nick
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ConstraintKinds and default associated empty constraints
Just a note: as section 6 of [1] notes, one way (possibly the only?)
to satisfy a universally quantified constraint would be a suitably
polymorphic instance — i.e. with a type variable in the head. I think
this would mitigate the need for whole program analysis at least in
some cases, including our current Functor example.
On the other hand, the Empty class does nicely avoid this entire
problem for this particular case.
[1] — http://www.haskell.org/haskellwiki/Quantified_contexts
On Mon, Jan 9, 2012 at 10:44 AM, Gábor Lehel illiss...@gmail.com wrote:
On Mon, Jan 9, 2012 at 4:53 PM, Simon Peyton-Jones
simo...@microsoft.com wrote:
Three things about this ConstraintKinds thread:
First, about
class Functor f where
type C f a :: Constraint
type C f a = ()
vs
class Functor f where
type C f :: * - Constraint
type C f = \_ - ()
I don't know any way of dealing in a decent way with the latter, because it
lacks type level lambdas. GHC currently allows only the former. I hope
that is enough. If not, perhaps give an example?
Second, it's true that the former would permit you to *index* on 'a' as well
as being parametric in 'a' (which is probably more what you intend). That's
a deficiency, but it's largely a notational one. Maybe there should be some
way to specify in a type family definition that some parameters can't be
used for indexing. It's orthogonal to the question of Constraint kinds, or
of defaults for associated types.
Third, () does indeed stand both for the unit tuple and for the empty
constraint, depending on context. So the code below works fine with HEAD.
I think it's ok with the 7.4 branch too, but it would be safer if someone
would check that. I included a test for the case tha Antoine found an error
with, namely
Could not deduce (FC [] Int) arising from a use of `fmap'
Simon
===
{-# LANGUAGE ConstraintKinds, TypeFamilies, FlexibleInstances #-}
module CK where
import GHC.Prim (Constraint)
import Prelude hiding (Functor, fmap)
import Data.Set (Set)
import qualified Data.Set as S (map, fromList)
class Functor f where
type C f a :: Constraint
type C f a = ()
fmap :: (C f a, C f b) = (a - b) - f a - f b
instance Functor Set where
type C Set a = Ord a
fmap = S.map
instance Functor [] where
fmap = map
testList = fmap (+1) [1,2,3]
testSet = fmap (+1) (S.fromList [1,2,3])
test2 = fmap (+1) [1::Int]
The problem with this is that you can't write, for example:
type OldFunctor f = (Functor f, forall a. C (f a) ~ ())
(If we had quantified contexts[1], then maybe, but we don't, and it
doesn't seem like it would be even theoretically possible for indexed
constraints without whole program analysis.)
With the other solution, though, you can write:
type OldFunctor f = (Functor f, C f ~ Empty) -- (In the real world I'd
rather call these Functor and Exofunctor...)
Again, I have no problem at all with the Empty class, it's the same
solution I've used. It's even kind polymorphic if you turn that
extension on. The syntax isn't superficially as nice, but it's nice
enough, does the job, and I don't see how you could do better short of
adding type-level lambdas (so you can write type C f = \_ - ()).
[1] http://hackage.haskell.org/trac/ghc/ticket/2893
| -Original Message-
| From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-
| users-boun...@haskell.org] On Behalf Of Andres Löh
| Sent: 09 January 2012 07:28
| To: Antoine Latter
| Cc: glasgow-haskell-users@haskell.org
| Subject: Re: ConstraintKinds and default associated empty constraints
|
| Hi.
|
| The definitions are accepted by GHC:
|
| class Functor f where
| type FC f a :: Constraint
| type FC f a = ()
|
| fmap :: (FC f a, FC f b) = (a - b) - f a - f b
|
| instance Functor [] where
| fmap = map
|
| Yes. This is what I would have expected to work.
|
| But I don't like the 'a' being an index parameter, and then the
| following expression:
|
| fmap (+1) [1::Int]
|
| Gives the error:
|
| Could not deduce (FC [] Int) arising from a use of `fmap'
| In the expression: fmap (+ 1) [1 :: Int]
| In an equation for `it': it = fmap (+ 1) [1 :: Int]
|
| gives the error:
|
| Number of parameters must match family declaration; expected 1
| In the type synonym instance default declaration for `FC'
| In the class declaration for `Functor'
|
| I get the same error, but it looks like a bug to me: If I move the
| declaration
|
| type FC f a = ()
|
| to the instance, then the example passes.
|
| Cheers,
| Andres
|
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
Disclaimer: this use case for type-level string ops is still hypothetical, so these are predictions. Shooting for the moon, I foresee writing a type-level string similarity metric. In my experience, that would involve nested traversals, sliding of sequence windows, etc. In that case, I would very much like to write the similarity measure algorithm as if the labels were a sequence of characters. The kind in the following signature assumes promoted lists and — though I know it's still up in the air — some sort of promotion of characters as Char. type LabelToLetters :: Label - [Char] Alternatively, the Char kind could simply be Label with an extralingual invariant that it has one character in it — though that doesn't smell like Haskell. The resulting kind of LabelToLetters in this case would be (Label - [Label]). A class of dumber algorithms for comparing type-level promotions of constructor names might simply attach some prefix or suffix and then test for equality. In that case, I'd just need append. type LabelAppend :: Label - Label - Label I personally lean towards LabelToLetters, since I predict that any direct interface for labels-as-sequences is going to perpetually be a subset of whatever becomes established as the interface for type-level lists. The symmetric LettersToLabel would be nice for balance, but I don't foresee needing it in this use case, since comparing Labels is more so a consumer of Labels as opposed to a producer. Whatever the interface to Labels, I would need to be able to test type-level characters for equality. While built-in decidable type equality family that returns a type of kind Bool would be fantastic (or preferably GHC ticket 1894), I'm not anticipating that anytime soon. In order to continue using my own library for such a type-level type equality predicate, I need to be able to provide type family instances for the type-level characters. I need type-level characters to be valid as indices in type family instances. That's all I foresee. Thanks. On Tue, Jan 3, 2012 at 3:32 AM, Simon Peyton-Jones simo...@microsoft.com wrote: | In regard to Labels versus Atom, etc., in my use case of converting | between similar datatypes, it would be very reasonable to eventually | add/remove prefixes/suffixes from these type-level reifications of | constructor names. If type-level strings are not implemented as lists | of characters, I would still like access to a comparable API. Can you be specific? What operations, exactly, do you want? Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
I'm interested in type-level strings myself. I'm using an approximation in order to enrich the instant-generics-style reflection of data type declarations with a sensitivity to constructor names. For example, this lets me automatically convert between many the similarly-named constructors of related data types (e.g. pipeline of ASTs in a compiler). Is there any existing developments regarding type-level strings? I have (arbitrarily) taken the approach of promoting the cereal library to the type-level, encoding strings that way, and working from there (ultimately inspired by Kiselyov and Chan's implicit configurations paper). It's certainly not perfect, but it's all I need for the functionality I've been chasing so far. In regard to Labels versus Atom, etc., in my use case of converting between similar datatypes, it would be very reasonable to eventually add/remove prefixes/suffixes from these type-level reifications of constructor names. If type-level strings are not implemented as lists of characters, I would still like access to a comparable API. Perhaps an isomorphism? Thanks for your time,Nick PS — I suspect the reflect to value-level idea was something along the lines of automatically providing a function @stringVal :: forall (a :: Label). a - String@. On Mon, Jan 2, 2012 at 6:38 AM, Simon Peyton-Jones simo...@microsoft.com wrote: It seems to me that there's only one essential missing language feature, which is appropriately-kinded type-level strings (and, ideally, the ability to reflect these strings back down to the value level). Given that, template haskell, and the HList bag of tricks, I'm confident that a fair number of elegant records packages can be crafted. Based on that experience, we can then decide what syntactic sugar would be useful to elide the TH layer altogether. I think we can do this part without much trouble, once the dust has settled on -XPolyKinds. It certainly fits with all the work we’ve been doing recently on the kind system. I agree that it’s a fairly basic requirement; for example, it’s also assumed by http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields Specifically · Allow String as a new kind · Now you can define classes or types with kinds like MyCls :: String - a - Constraint T :: String - * · Provide type-level string literals, so that “foo” :: String Open questions: · Is String (at the kind level) a synonym for [Char]? I’m inclined *not* to do this initially, because it would require us to have promoted character literals too -- and the implementation of record labels as strings of type-level cons-cells is not going to be efficient. · If String is not a kind level synonym for [Char], maybe it should have a different name. For example, “foo” :: Label? Or Atom? After all, if it doesn’t behave like a Haskell string it probably should not have the same name. · Are there any operations over Labels? · I don’t know exactly what you have in mean by “the ability to reflect the type-level string at the value level”. Simon From: Gershom Bazerman [mailto:gersh...@gmail.com] Sent: 31 December 2011 19:12 To: Simon Peyton-Jones Cc: Greg Weber; glasgow-haskell-users@haskell.org Subject: Re: Records in Haskell On Dec 31, 2011, at 1:28 PM, Simon Peyton-Jones wrote: The trouble is that I just don't have the bandwidth (or, if I'm honest, the motivation) to drive this through to a conclusion. And if no one else does either, perhaps it isn't *that* important to anyone. That said, it clearly is *somewhat* important to a lot of people, so doing nothing isn't very satisfactory either. Usually I feel I know how to move forward, but here I don't. Simon It seems to me that there's only one essential missing language feature, which is appropriately-kinded type-level strings (and, ideally, the ability to reflect these strings back down to the value level). Given that, template haskell, and the HList bag of tricks, I'm confident that a fair number of elegant records packages can be crafted. Based on that experience, we can then decide what syntactic sugar would be useful to elide the TH layer altogether. Beyond that, it would really help namespacing in general to appropriately extend the module system to allow multiple modules to be declared within a single file -- or, better yet, submodules. I know that this introduces a few corner cases that need to be thought through -- what happens with overlapping declarations, for example. But I tend to think the path here is relatively straightforward and obvious, and the added expressive power should make namespacing issues much more tractable. Like the type-level strings proposal, this isn't about implementing records as such -- rather, it's about generally extending the expressive power of the language so that record systems--among other things--are easier to write. Cheers,
Superclass Cycle via Associated Type
(Sorry I'm so late to this dialogue.)
In http://www.haskell.org/pipermail/glasgow-haskell-users/2011-July/020593.html,
SPJ asks
The superclasses are recursive but
a) They constrain only type variables
b) The variables in the superclass context are all
mentioned in the head. In class Q = C a b c
fv(Q) is subset of {a,b,c}
Question to all: is that enough?
I just recently came upon my own desire for this capability, but I'm
pretty sure my reply to SPJ's question is No. I'd like to extend
Sat's modeling capabilities to also cover superclass constraints.
type family Super a
class Sat (Super a) = Sat a where dict :: a
This seems to necessitate recursive dictionaries — I'm not familiar
enough with the dictionary-implementation details to understand how
much of an understatement that might be. All I can say is that my own
intuitions about those things don't yet deem this technique
infeasible.
Let's take a reification of Ord as an example.
data EmptyD a = EmptyD
type instance Super (EmptyD a) = EmptyD a
instance Sat (EmptyD a) where dict = EmptyD
data EqD a where EqD :: Eq a = EqD a
type instance Super (EqD a) = EmptyD a
instance Eq a = Sat (EqD a) where dict = EqD
data OrdD a where OrdD :: Ord a = OrdD a
type instance Super (OrdD a) = EqD a
instance Ord a = Sat (OrdD a) where dict = OrdD
Now GHC can derive Sat (EqD a) from Sat (OrdD a). I'd bet this could
be cleaned via Constraint Kinds [1] — if not totally subsumed by them:
type family Super a :: Constraint
class Super a = Sat a where dict :: a
data OrdD a where OrdD :: Ord a = OrdD a
type instance Super (OrdD a) = Ord a
instance Ord a = Sat (OrdD a) where dict = OrdD
With these definitions, there'd be an isomorphism between Sat (OrdD a)
and Ord a. I don't know how difficult it would be for GHC to wield
that isomorphism.
At this point, though, perhaps Constraint Kinds simply deprecate Sat?
[1] does, after all, define one reified dictionary to rule them all.
-
[1] - http://blog.omega-prime.co.uk/?p=127
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
