Re: [GHC] #9898: Wanted: higher-order type-level programming

18 Dec 2014

      #9898: Wanted: higher-order type-level programming
-------------------------------------+-------------------------------------
              Reporter:  erisco      |            Owner:
                  Type:  feature     |           Status:  new
  request                            |        Milestone:
              Priority:  normal      |          Version:  7.8.3
             Component:  Compiler    |         Keywords:
  (Type checker)                     |     Architecture:  x86_64 (amd64)
            Resolution:              |       Difficulty:  Unknown
      Operating System:  Windows     |       Blocked By:
       Type of failure:  GHC         |  Related Tickets:
  rejects valid program              |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by erisco):

 Does applying a type family to no arguments count as being partially
 applied? i.e. will such usage be banned n 7.8.4? So far 7.8.3 seems to
 make correct inferences in such cases. If this breaks in 7.8.4 I would
 like to know so that I do not write a lot of code that depends on it.
 Compiling GHC does not appear to be a small task otherwise I would test it
 myself.

 Here is an example where it is relevant. Maybe there is a better
 implementation. A usage may be `F EvalEqual :. F (Equal Int) :: Fun *
 Bool` which can then be used as a predicate for filtering a type list, for
 example. Of course a possible problem is that `EvalEqual` may be
 considered partially applied and rejected by 7.8.4 even though this
 appears to work fine in 7.8.3 (i.e. inference appears to be working fine).

 {{{
 data Equal' where
   Equal :: x -> y -> Equal'

 type family EvalEqual (x :: Equal') :: Bool where
   EvalEqual (Equal x x) = True
   EvalEqual (Equal x y) = False
 }}}

 For completeness here are the other definitions, and I include `:$` as
 well. Not sure if this is the way to do function composition but this is
 the best I have after a few failed attempts.

 {{{
 data Fun a b where
   F :: (a -> b) -> Fun a b
   (.:) :: Fun b c -> Fun a b -> Fun a c

 type family (f :: Fun ka kb) :$ (x :: ka) where
   (f .: g) :$ x = g :$ (f :$ x)
   (F f) :$ x = f x
 }}}

 What is a good place for Q&A on type level programming in Haskell?
 Obviously the GHC bug tracker is not it. I have tried the #haskell IRC
 channel but there are only a few people there that understand this area
 and I can seldom get their attention.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:4
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler