Opened 5 years ago

Last modified 2 years ago

#9898 new feature request

Wanted: higher-order type-level programming

Reported by: erisco Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: TypeFamilies Cc: kcsongor
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

'test3' is expected to type check given that 'test1' and 'test2' type check. 'test4' is not expected to type check.

ghc_bug2.hs:24:9:
    Couldn't match type `(Char, ())' with `()'
    Expected type: Filter (Equal Int) (Char, Filter (Equal Int) ())
      Actual type: ()
    In the expression:
        () :: Filter (Equal Int) (Char, Filter (Equal Int) ())
    In an equation for `test2':
        test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())

ghc_bug2.hs:28:9:
    Couldn't match type `(Char, ())' with `()'
    Expected type: Filter (Equal Int) (Char, ())
      Actual type: ()
    In the expression: ()
    In an equation for `test3': test3 = ()
{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds #-}
module Main where

type family Filter f xs where
  Filter f (x, xs) = ApplyFilter (f x) (x, Filter f xs)
  Filter f () = ()
--

type family ApplyFilter p xs where
  ApplyFilter False (x, xs) = xs
  ApplyFilter p xs = xs
--

type family Equal x y where
  Equal x x = True
  Equal x y = False
--

-- Type checks
test1 :: ApplyFilter ((Equal Int) Char) (Char, Filter (Equal Int) ())
test1 = ()

-- Couldn't match type `(Char, ())' with `()'
test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())

-- Couldn't match type `(Char, ())' with `()'
test3 :: Filter (Equal Int) (Char, ())
test3 = ()

-- Type checks, should not
test4 :: Filter (Equal Int) (Char, ())
test4 = ('x', ())

Change History (11)

comment:1 Changed 5 years ago by simonpj

Summary: Couldn't match type `(Char, ())' with `()'Wanted: higher-order type-level programming
Type: bugfeature request

HEAD correctly says

T9898.hs:20:10:
    Type family ‘Equal’ should have 2 arguments, but has been given 1
    In the type signature for ‘test1’:
      test1 :: ApplyFilter ((Equal Int) Char) (Char,
                                               Filter (Equal Int) ())

T9898.hs:27:10:
    Type family ‘Equal’ should have 2 arguments, but has been given 1
    In the type signature for ‘test3’:
      test3 :: Filter (Equal Int) (Char, ())

T9898.hs:31:10:
    Type family ‘Equal’ should have 2 arguments, but has been given 1
    In the type signature for ‘test4’:
      test4 :: Filter (Equal Int) (Char, ())

You can't partially apply a type function, I'm afraid. Yes, that limits higher-order programming. Better solutions (that still support type inference) most welcome.

I'll leave this open as a feature request for higher order type level programming.

Simon

comment:2 Changed 5 years ago by erisco

Thanks Simon. I was mislead by the problem reported in issue #9433.

comment:3 Changed 5 years ago by goldfire

Though I'm all for fixing this so that it's possible in GHC, you may also want to check out the singletons package, which goes to lengths to emulate this feature. See also the related paper here.

One of these years, I hope to push for adoption of some of the ideas from that paper into GHC proper -- without defunctionalization, for sure. See sections 7.2 and 7.5.

comment:4 Changed 5 years ago 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. A key point is that Equal (promoted) is a type constructor which, from my understanding, is allowed to be partially applied. However, a possible problem is that the type family 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.

Last edited 5 years ago by erisco (previous) (diff)

comment:5 Changed 5 years ago by jstolarek

Does applying a type family to no arguments count as being partially applied?

Yes. To be more precise: you can't have *unsaturated* type families, where unsaturated means "applied to less arguments than it's arity".

will such usage be banned n 7.8.4?

No. But that's still a bug and you shouldn't construct your code around this.

What is a good place for Q&A on type level programming in Haskell?

Haskell-cafe.

If you really want partial application at the type level you can try out singletons, as suggested by Richard.

comment:6 in reply to:  5 ; Changed 5 years ago by rwbarton

Replying to jstolarek:

will such usage be banned n 7.8.4?

No. But that's still a bug and you shouldn't construct your code around this.

Really? #9433 is marked as merged as 7.8.4, or am I misunderstanding something here? Or is there a distinction between the "applied to zero arguments" case and the "applied to at least one, but fewer than its arity" case?

comment:7 in reply to:  6 Changed 5 years ago by jstolarek

Replying to rwbarton:

Really? #9433 is marked as merged as 7.8.4

You're right. In that case this behaviour will change in GHC 7.8.4. I don't know why, but my impression was that 7.8.4 will only address some critical LLVM bug.

Or is there a distinction between the "applied to zero arguments" case and the "applied to at least one, but fewer than its arity" case?

No, that's the same.

comment:8 Changed 4 years ago by thomie

Architecture: x86_64 (amd64)Unknown/Multiple
Operating System: WindowsUnknown/Multiple

comment:9 Changed 4 years ago by mpickering

Cc: kcsongor added

comment:10 Changed 2 years ago by RyanGlScott

See also this GHC proposal on partially applied type families, which is quite relevant here.

comment:11 Changed 2 years ago by RyanGlScott

Keywords: TypeFamilies added
Note: See TracTickets for help on using tickets.