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
Summary: | Couldn't match type `(Char, ())' with `()' → Wanted: higher-order type-level programming |
---|---|
Type: | bug → feature request |
comment:2 Changed 5 years ago by
Thanks Simon. I was mislead by the problem reported in issue #9433.
comment:3 Changed 5 years ago by
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
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.
comment:5 follow-up: 6 Changed 5 years ago by
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 follow-up: 7 Changed 5 years ago by
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 Changed 5 years ago by
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
Architecture: | x86_64 (amd64) → Unknown/Multiple |
---|---|
Operating System: | Windows → Unknown/Multiple |
comment:9 Changed 4 years ago by
Cc: | kcsongor added |
---|
comment:10 Changed 2 years ago by
See also this GHC proposal on partially applied type families, which is quite relevant here.
comment:11 Changed 2 years ago by
Keywords: | TypeFamilies added |
---|
HEAD correctly says
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