GHC on OpenIndiana

2012-09-16 Thread asyropoulos

Dear Developers,

  I am trying to compile the GHC on OpenIndiana (essentially Solaris 
11).  I follow the steps in


http://www.haskell.org/ghc/docs/6.4.1/html/building/sec-porting-ghc.html#sec-booting-from-hc

and here is what I get:

$ ./distrib/hc-build --prefix=/opt/gnu/ghcb --enable-hc-boot
*** Building compiler...
checking for gfind... /usr/bin/gfind
checking for sort... /opt/gnu/bin/sort
checking for ghc... no
checking build system type... i386-pc-solaris2.11
checking host system type... i386-pc-solaris2.11
checking target system type... i386-pc-solaris2.11
HOST: i386-pc-solaris2.11
Can't work out build platform


Not e that configure.ac contains a section on Solaris:

SOLARIS_BROKEN_SHLD=NO

case $host in
i386-*-solaris2)
# here we go with the test
MINOR=`uname -r|cut -d '.' -f 2-`
if test $MINOR -lt 11; then
   SOLARIS_BROKEN_SHLD=YES
fi
;;
esac

For whatever the reason I  need to update configure.in to recognise 
the new architecture, and re-generate configure with autoreconf
but I have no idea what exactly to add. There is no template inside to 
help me. Could you please let me know what should I do to

proceed?

Thank you in advance for your help/suggestions.

A.S.

--
Apostolos Syropoulos
Xanthi, Greece



___
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?

2012-09-16 Thread Simon Peyton-Jones
Friends

Thanks for this useful conversation, by email and at ICFP.  Here's my summary.  
Please tell me if I'm on the right track.  It would be great if someone wanted 
to create a page on the GHC wiki to capture the issues and outcomes.

Simon

Eta rules
~~
*   We want to add eta-rules to FC.  Sticking to pairs for now, that would 
amount to
 adding two new type functions (Fst, Snd), and three new, built-in axioms
axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
 Generalising to arbitrary products looks feasible.

*  Adding these axioms would make FC inconsistent, because 
axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
 and that has two different type constructors on each side.
 However, I think is readily solved: see below under Fixing Any

* Even in the absence of Any, it's not 100% obvious that adding the above
   eta axioms retains consistency of FC.  I believe that Richard is volunteering
   to check this out.  Right, Richard?

Type inference
~
I'm a little unclear about the implications for inference.  One route
might be this.   Suppose we are trying to solve a constraint
 [W]  (a:'(k1,ks)) ~ '( t1, t2 )
where a is an untouchable type variable.  (if it was touchable we'd
simply unify it.)  Then we can replace it with a constraint
[W]   '(Fst a, Snd a) ~ '( t1, t2)

Is that it?  Or do we need more?  I'm a bit concerned about constraints like
F a ~ e
where a:'(k1,k2), and we have a type instance like  F '(a,b) = ...

Anything else?

I don't really want to eagerly eta-expand every type variable, because (a) 
we'll bloat the constraints and (b) we might get silly error messages.  For (b) 
consider the insoluble constraint
[W]  a~b
where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll 
get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b), and we 
DEFINITELY don't want to report that as a type error!

Fixing Any
~~~
* I think we can fix the Any problem readily by making Any into a type family, 
 that has no instances.   We certainly allow equalities with a type
 *family* application on the left and a type constructor on the right.
 I have implemented this change already... it seems like a good plan.

* Several people have asked why we need Any at all.  Consider this source 
program
 reverse []
 At what type should we instantiate 'reverse' and the empty list []?  Any 
type
 will do, but we must choose one; FC doesn't have unbound type variables.
 So I instantiate it at (Any *):
 reverse (Any *) ([] (Any *))

 Why is Any poly-kinded?  Because the above ambiguity situation sometimes 
 arises at other kinds.

*   I'm betting that making Any into a family will mess up Richard's (entirely 
separate)
 use of (Any k) as a proxy for a kind argument k; because now (Any k1 ~ Any 
k2)
 does not entail (k1~k2).   We need Any to be an *injective* type family.  
We want
 injective type families anyway, so I guess I should add the internal 
machinery 
 (which is easy).

 I believe that injective type families are fully decomposable, just like 
data type families,
 correct?  To make them available at the source level, we'd just need to
   a) add the syntax injective type family F a :: *
   b) check for injectivity when the user adds type instances
 Richard, would you like to do that part?



___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: GHC on OpenIndiana

2012-09-16 Thread John Wiegley
 asyropoulos  asyropou...@aol.com writes:

 I am trying to compile the GHC on OpenIndiana (essentially Solaris 11).  I
 follow the steps in

Hi Apostolos,

It took me a while to finally figure this out, but in the end I was able to
get GHC 7.4.2 working nicely on OpenIndiana.  Here are the steps I followed:

 1. Add the SFE publisher to OpenIndiana

pkg set-publisher -p http://pkg.openindiana.org/sfe

 2. Uninstall the old gnu and gcc-3 packages

 3. Install gcc@4.6.2 from SFE (or whatever is current)

 4. Configure with:

./configure '--with-ld=/usr/bin/ld --with-gcc=/usr/bin/gcc \
--with-nm=/usr/bin/nm --with-gmp-includes=/usr/gnu/include \
--with-gmp-libraries=/usr/gnu/lib \
--with-iconv-includes=/usr/gnu/include \
--with-iconv-libraries=/usr/gnu/lib

 5. make

Here are my fulltest results:

OVERALL SUMMARY for test run started at Thu Sep  6 14:54:28 CDT 2012
3402 total tests, which gave rise to
   16613 test cases, of which
   0 caused framework failures
3554 were skipped

   12513 expected passes
 367 had missing libraries
 133 expected failures
   0 unexpected passes
  46 unexpected failures

Unexpected failures:
   ../../libraries/base/tests/Concurrent  ThreadDelay001 [bad stdout or stderr] 
(ghci)
   ../../libraries/base/tests/IO  hGetBuf001 [bad exit code] (ghci)
   ../../libraries/process/tests  1780 [bad exit code] (ghci)
   ../../libraries/process/tests  process005 [bad exit code] (ghci)
   ../../libraries/unix/tests signals002 [bad exit code] (ghci)
   ../../libraries/unix/tests signals004 [bad exit code] 
(ghci,threaded1,threaded2,profthreaded)
   ../../libraries/unix/tests/libposixposix002 [bad stdout] 
(normal,hpc,optasm,threaded1,threaded2,dyn,optllvm)
   ../../libraries/unix/tests/libposixposix002 [bad stdout or stderr] (ghci)
   codeGen/should_run cgrun071 [bad exit code] 
(normal,hpc,optasm,profasm,ghci,threaded1,threaded2,dyn,profthreaded,g1)
   concurrent/should_run  async001 [bad stdout or stderr] (ghci)
   concurrent/should_run  conc058 [bad stdout or stderr] (ghci)
   concurrent/should_run  conc070 [bad stdout or stderr] (ghci)
   concurrent/should_run  foreignInterruptible [bad exit code] 
(ghci)
   driver/objcobjc-hi [bad profile] (profthreaded)
   driver/objcobjc-hi [bad heap profile] (profasm)
   driver/objcobjcpp-hi [bad profile] (profthreaded)
   driver/objcobjcpp-hi [bad heap profile] (profasm)
   ghci/should_run3171 [bad stdout] (normal)
   perf/compiler  T4801 [stat too good] (normal)
   perf/compiler  T6048 [stat not good enough] (optasm)
   perf/compiler  T783 [stat not good enough] (normal)
   perf/haddock   haddock.Cabal [stat not good enough] 
(normal)
   perf/haddock   haddock.base [stat not good enough] 
(normal)
   perf/haddock   haddock.compiler [stat not good 
enough] (normal)
   rtsderefnull [bad profile] 
(profasm,profthreaded)
   rtsdivbyzero [bad profile] 
(profasm,profthreaded)

John

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


Re: Type operators in GHC

2012-09-16 Thread Conal Elliott
Hm. ~ is a sometimes-fine prefix for abstracting over arrowish things,
but perhaps not so appealing for others doing pairish, sumish etc
abstractions.

-- Conal

On Sat, Sep 15, 2012 at 4:47 AM, Sjoerd Visscher sjo...@w3future.comwrote:

 +1. Making : the signal for type variables would break even more code,
 f.e. fclabels.

 ~ almost means variable, so I'd like that as a prefix.

 Sjoerd

 On Sep 15, 2012, at 2:09 AM, Cale Gibbard cgibb...@gmail.com wrote:

  There's a fair amount of code out there which uses (~) as a type
  variable (we have ~10k lines of heavy arrow code at iPwn). It would be
  *really* nice if that could be accommodated somehow. But the proposal
  you just gave at least would allow for a textual substitution, so not
  quite so bad as having to change everything to prefix notation.
 
  On 14 September 2012 19:26, Simon Peyton-Jones simo...@microsoft.com
 wrote:
  Fair point.  So you are saying it’d be ok to say
 
 
 
   data T (.-)  = MkT (Int .- Int)
 
 
 
  where (.+) is a type variable?   Leaving ordinary (+) available for type
  constructors.
 
 
 
  If we are inverting the convention I wonder whether we might invert it
  completely and use “:” as the “I’m different” herald as we do for
  *constructor* operators in terms.  Thus
 
 
 
   data T (:-)  = MkT (Int :- Int)
 
 
 
  That seems symmetrical, and perhaps nicer than having a new notation.
 
 
 
  In terms  In types
 
  ---
 
  aTerm variable Type variable
 
  AData constructor Type constructor
 
  +Term variable operator   Type constructor operator
 
  :+  Data constructor operator   Type variable operator
 
 
 
  Any other opinions?
 
 
 
  Simon
 
 
 
  From: conal.elli...@gmail.com [mailto:conal.elli...@gmail.com] On
 Behalf Of
  Conal Elliott
  Sent: 06 September 2012 23:59
  To: Simon Peyton-Jones
  Cc: GHC users
  Subject: Re: Type operators in GHC
 
 
 
  Oh dear. I'm very sorry to have missed this discussion back in January.
 I'd
  be awfully sad to lose pretty infix notation for type variables of kind
 * -
  * - *. I use them extensively in my libraries and projects, and pretty
  notation matters.
 
  I'd be okay switching to some convention other than lack of leading ':'
 for
  signaling that a symbol is a type variable rather than constructor,
 e.g.,
  the *presence* of a leading character such as '.'.
 
  Given the increasing use of arrow-ish techniques and of type-level
  programming, I would not classify the up-to-7.4 behavior as a foolish
  consistency, especially going forward.
 
  -- Conal
 
  On Wed, Jan 18, 2012 at 6:27 AM, Simon Peyton-Jones 
 simo...@microsoft.com
  wrote:
 
  Dear GHC users
 
  As part of beefing up the kind system, we plan to implement the Type
  operators proposal for Haskell Prime
 
 http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors
 
  GHC has had type operators for some kind, so you can say
 data a :+: b = Left a | Right b
  but you can only do that for operators which start with :.
 
  As part of the above wiki page you can see the proposal to broaden this
 to
  ALL operators, allowing
 data a + b = Left a | Right b
 
  Although this technically inconsistent the value page (as the wiki page
  discussed), I think the payoff is huge. (And A foolish consistency is
 the
  hobgoblin of little minds, Emerson)
 
 
  This email is (a) to highlight the plan, and (b) to ask about flags.
  Our
  preferred approach is to *change* what -XTypeOperators does, to allow
 type
  operators that do not start with :.  But that will mean that *some*
  (strange) programs will stop working. The only example I have seen in
 tc192
  of GHC's test suite
 {-# LANGUAGE TypeOperators #-}
 comp :: Arrow (~) = (b~c, c~d)~(b~d)
   comp = arr (uncurry ())
 
  Written more conventionally, the signature would look like
 comp :: Arrow arr = arr (arr b c, arr c d) (arr b d)
   comp = arr (uncurry ())
  or, in infix notation
 {-# LANGUAGE TypeOperators #-}
 comp :: Arrow arr = (b `arr` c, c `arr` d) `arr` (b `arr` d)
   comp = arr (uncurry ())
 
  But tc192 as it stands would become ILLEGAL, because (~) would be a
 type
  *constructor* rather than (as now) a type *variable*.  Of course it's
 easily
  fixed, as above, but still a breakage is a breakage.
 
  It would be possible to have two flags, so as to get
   - Haskell 98 behaviour
   - Current TypeOperator behaviuor
   - New TypeOperator behaviour
  but it turns out to be Quite Tiresome to do so, and I would much rather
 not.
  Can you live with that?
 
 
 
 http://chrisdone.com/posts/2010-10-07-haskelldb-and-typeoperator-madness.html
 
 
  ___
  Glasgow-haskell-users mailing list
  Glasgow-haskell-users@haskell.org
  

Re: Type operators in GHC

2012-09-16 Thread Conal Elliott
I also have quite a lot of code (growing daily) that uses (~) as a type
variable. It's not the only such type variable, because some abstractions
are about combining multiple arrowish things, e.g., more CT variations on
Functor and Foldable that allow valuable flexibility missing in the
standard library. In those cases, I typically use (+) and (--) as well.

-- Conal

On Fri, Sep 14, 2012 at 5:09 PM, Cale Gibbard cgibb...@gmail.com wrote:

 There's a fair amount of code out there which uses (~) as a type
 variable (we have ~10k lines of heavy arrow code at iPwn). It would be
 *really* nice if that could be accommodated somehow. But the proposal
 you just gave at least would allow for a textual substitution, so not
 quite so bad as having to change everything to prefix notation.

 On 14 September 2012 19:26, Simon Peyton-Jones simo...@microsoft.com
 wrote:
  Fair point.  So you are saying it’d be ok to say
 
 
 
data T (.-)  = MkT (Int .- Int)
 
 
 
  where (.+) is a type variable?   Leaving ordinary (+) available for type
  constructors.
 
 
 
  If we are inverting the convention I wonder whether we might invert it
  completely and use “:” as the “I’m different” herald as we do for
  *constructor* operators in terms.  Thus
 
 
 
data T (:-)  = MkT (Int :- Int)
 
 
 
  That seems symmetrical, and perhaps nicer than having a new notation.
 
 
 
   In terms  In types
 
  ---
 
  aTerm variable Type variable
 
  AData constructor Type constructor
 
  +Term variable operator   Type constructor operator
 
  :+  Data constructor operator   Type variable operator
 
 
 
  Any other opinions?
 
 
 
  Simon
 
 
 
  From: conal.elli...@gmail.com [mailto:conal.elli...@gmail.com] On
 Behalf Of
  Conal Elliott
  Sent: 06 September 2012 23:59
  To: Simon Peyton-Jones
  Cc: GHC users
  Subject: Re: Type operators in GHC
 
 
 
  Oh dear. I'm very sorry to have missed this discussion back in January.
 I'd
  be awfully sad to lose pretty infix notation for type variables of kind
 * -
  * - *. I use them extensively in my libraries and projects, and pretty
  notation matters.
 
  I'd be okay switching to some convention other than lack of leading ':'
 for
  signaling that a symbol is a type variable rather than constructor, e.g.,
  the *presence* of a leading character such as '.'.
 
  Given the increasing use of arrow-ish techniques and of type-level
  programming, I would not classify the up-to-7.4 behavior as a foolish
  consistency, especially going forward.
 
  -- Conal
 
  On Wed, Jan 18, 2012 at 6:27 AM, Simon Peyton-Jones 
 simo...@microsoft.com
  wrote:
 
  Dear GHC users
 
  As part of beefing up the kind system, we plan to implement the Type
  operators proposal for Haskell Prime
  http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors
 
  GHC has had type operators for some kind, so you can say
  data a :+: b = Left a | Right b
  but you can only do that for operators which start with :.
 
  As part of the above wiki page you can see the proposal to broaden this
 to
  ALL operators, allowing
  data a + b = Left a | Right b
 
  Although this technically inconsistent the value page (as the wiki page
  discussed), I think the payoff is huge. (And A foolish consistency is
 the
  hobgoblin of little minds, Emerson)
 
 
  This email is (a) to highlight the plan, and (b) to ask about flags.  Our
  preferred approach is to *change* what -XTypeOperators does, to allow
 type
  operators that do not start with :.  But that will mean that *some*
  (strange) programs will stop working. The only example I have seen in
 tc192
  of GHC's test suite
  {-# LANGUAGE TypeOperators #-}
  comp :: Arrow (~) = (b~c, c~d)~(b~d)
comp = arr (uncurry ())
 
  Written more conventionally, the signature would look like
  comp :: Arrow arr = arr (arr b c, arr c d) (arr b d)
comp = arr (uncurry ())
  or, in infix notation
  {-# LANGUAGE TypeOperators #-}
  comp :: Arrow arr = (b `arr` c, c `arr` d) `arr` (b `arr` d)
comp = arr (uncurry ())
 
  But tc192 as it stands would become ILLEGAL, because (~) would be a type
  *constructor* rather than (as now) a type *variable*.  Of course it's
 easily
  fixed, as above, but still a breakage is a breakage.
 
  It would be possible to have two flags, so as to get
- Haskell 98 behaviour
- Current TypeOperator behaviuor
- New TypeOperator behaviour
  but it turns out to be Quite Tiresome to do so, and I would much rather
 not.
  Can you live with that?
 
 
 
 http://chrisdone.com/posts/2010-10-07-haskelldb-and-typeoperator-madness.html
 
 
  ___
  Glasgow-haskell-users mailing list
  Glasgow-haskell-users@haskell.org
  

Re: Type operators in GHC

2012-09-16 Thread Conal Elliott
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.

Better still for me personally would be for other libraries to add a
LANGUAGE pragma to get the 7.6.1 behavior. I can live without this option.

Using a : prefix for type ctor variables would break the other half of my
types in these libraries. I use type variables with names like (~), (+),
(--) etc in order to express abstractions, and then I typically use those
abstractions to define concrete type ctors with names like (:-), (:+),
(:--), etc.

My regrets for raising these issues so late in the game.

-- Conal

On Fri, Sep 14, 2012 at 4:26 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:

  Fair point.  So you are saying it’d be ok to say

 ** **

   data T (.-)  = MkT (Int .- Int)

 ** **

 where (.+) is a type variable?   Leaving ordinary (+) available for type
 constructors.

 ** **

 If we are inverting the convention I wonder whether we might invert it
 completely and use “:” as the “I’m different” herald as we do for **
 constructor** operators in terms.  Thus

 ** **

   data T (:-)  = MkT (Int :- Int)

 ** **

 That seems symmetrical, and perhaps nicer than having a new notation.  ***
 *

 

  In terms  In types***
 *

 ---***
 *

 aTerm variable Type variable

 AData constructor Type constructor

 +Term variable operator   Type constructor operator***
 *

 :+  Data constructor operator   Type variable operator

 ** **

 Any other opinions?

 ** **

 Simon

 ** **

 *From:* conal.elli...@gmail.com [mailto:conal.elli...@gmail.com] *On
 Behalf Of *Conal Elliott
 *Sent:* 06 September 2012 23:59
 *To:* Simon Peyton-Jones
 *Cc:* GHC users
 *Subject:* Re: Type operators in GHC

 ** **

 Oh dear. I'm very sorry to have missed this discussion back in January.
 I'd be awfully sad to lose pretty infix notation for type variables of kind
 * - * - *. I use them extensively in my libraries and projects, and
 pretty notation matters.

 I'd be okay switching to some convention other than lack of leading ':'
 for signaling that a symbol is a type variable rather than constructor,
 e.g., the *presence* of a leading character such as '.'.

 Given the increasing use of arrow-ish techniques and of type-level
 programming, I would not classify the up-to-7.4 behavior as a foolish
 consistency, especially going forward.

 -- Conal

 

 On Wed, Jan 18, 2012 at 6:27 AM, Simon Peyton-Jones simo...@microsoft.com
 wrote:

 Dear GHC users

 As part of beefing up the kind system, we plan to implement the Type
 operators proposal for Haskell Prime
 http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors

 GHC has had type operators for some kind, so you can say
 data a :+: b = Left a | Right b
 but you can only do that for operators which start with :.

 As part of the above wiki page you can see the proposal to broaden this to
 ALL operators, allowing
 data a + b = Left a | Right b

 Although this technically inconsistent the value page (as the wiki page
 discussed), I think the payoff is huge. (And A foolish consistency is the
 hobgoblin of little minds, Emerson)


 This email is (a) to highlight the plan, and (b) to ask about flags.  Our
 preferred approach is to *change* what -XTypeOperators does, to allow type
 operators that do not start with :.  But that will mean that *some*
 (strange) programs will stop working. The only example I have seen in tc192
 of GHC's test suite
 {-# LANGUAGE TypeOperators #-}
 comp :: Arrow (~) = (b~c, c~d)~(b~d)
   comp = arr (uncurry ())

 Written more conventionally, the signature would look like
 comp :: Arrow arr = arr (arr b c, arr c d) (arr b d)
   comp = arr (uncurry ())
 or, in infix notation
 {-# LANGUAGE TypeOperators #-}
 comp :: Arrow arr = (b `arr` c, c `arr` d) `arr` (b `arr` d)
   comp = arr (uncurry ())

 But tc192 as it stands would become ILLEGAL, because (~) would be a type
 *constructor* rather than (as now) a type *variable*.  Of course it's
 easily fixed, as above, but still a breakage is a breakage.

 It would be possible to have two flags, so as to get
   - Haskell 98 behaviour
   - Current TypeOperator behaviuor
   - New TypeOperator behaviour
 but it turns out to be Quite Tiresome to do so, and I would much rather
 not.  Can you live with that?



 http://chrisdone.com/posts/2010-10-07-haskelldb-and-typeoperator-madness.html


 ___
 Glasgow-haskell-users mailing list
 Glasgow-haskell-users@haskell.org
 

Kind Demotion

2012-09-16 Thread Ashley Yakeley
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


Re: Kind Demotion

2012-09-16 Thread Richard Eisenberg
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


Re: Kind Demotion

2012-09-16 Thread Ashley Yakeley

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