Please excuse me if I use the wrong terminology, I am much a beginner in haskell type manipulation... I am trying to use overlapping instances with functional dependencies to do some type-level programming with HLists.
Here my objective is to try and write a typeclass HNoNils l l'
, where HNoNils l l'
means that, with l
being a list type (ex: Int : String : EmptyNil : Int : HNil
), l'
is the corresponding list type without the specific empty type EmptyNil
( result of example: Int:String:Int:HNil
):
{-# LANGUAGE ExistentialQuantification,
FunctionalDependencies,
FlexibleInstances,
UndecidableInstances,
OverlappingInstances,
TypeFamilies #-}
import Data.HList
import Data.TypeLevel.Bool
--Type Equality operators
--usedto check if a type is equal to another
class TtEq a b eq | a b -> eq
instance TtEq a a True
instance eq~False => TtEq a b eq
data EmptyNil = EmptyNil deriving (Show) --class representing empty channel
--class intended to generate a list type with no type of EmptyNil
-- Example: HCons Int $ HCons EmptyNil HNil should give HCons Int HNil
class (HList list, HList out) => HNoNils list out | list -> out
where hNoNils :: list -> out
-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l',TtEq e EmptyNil True ) => HNoNils (HCons e l) l'
where hNoNils (HCons e l) = hNoNils l
-- l gives l' means (HCons e l) gives (HCons e l') for all e
instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')
where hNoNils (HCons e l) = hCons e $ hNoNils l
--base case
instance HNoNils HNil HNil
where hNoNils _ = hNil
testList = HCons EmptyNil $ HCons EmptyNil HNil
testList1 = HCons "Hello" $ HCons EmptyNil HNil
testList2 = HCons EmptyNil $ HCons "World" HNil
testList3 = HCons "Hello" $ HCons "World" HNil
main:: IO ()
main = do
print $ hNoNils testList -- should get HNil
print $ hNoNils testList1 -- should get HCons "Hello" HNil
print $ hNoNils testList2 -- should get HCons "World" HNil
print $ hNoNils testList3 -- should get HCons "Hello" (HCons "World" HNil)
When I run this code as-is, however, all my hNoNils
calls seem to resolve through the least specific, second, instance declaration, meaning (at least it seems), that for all l
, I have HNoNils l l
.
Based off of what I have read, with the OverlappingInstances
extension, The system is supposed to always resolve to the most specific instance.
Here
the first instance has the constraints
(HNoNils l l',TtEq e EmptyNil True )
the second instance has the constraints
HNoNils l l'
Forgive me if I'm wrong, but it seems like the first instance is more specific than the second, so it should go for that one, right?
I have tried adding constraints to try and get rid of the overlap, namely by adding the seperate, oposite equality constraint to the second instance:
-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l',TtEq e EmptyNil True ) => HNoNils (HCons e l) l'
where hNoNils (HCons e l) = hNoNils l
-- l gives l' means (HCons e l) gives (HCons e l') for all e
-- added constraint of TtEq e EmptyNil False
instance (HNoNils l l',TtEq e EmptyNil False) => HNoNils (HCons e l) (HCons e l')
where hNoNils (HCons e l) = hCons e $ hNoNils l
I tried removing the overlapping instance extension here, and I'm getting overlap errors.
Overlapping instances for HNoNils
(HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l')
Matching instances:
instance (HNoNils l l', TtEq e EmptyNil True) =>
HNoNils (HCons e l) l'
-- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:32:10
instance (HNoNils l l', TtEq e EmptyNil False) =>
HNoNils (HCons e l) (HCons e l')
-- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:36:10
I don't understand the second match. After all, in this resolution, we have e equal to EmptyNil, so TtEq e EmptyNil True
... right? And for that matter, how does the type system even get to a situation where it's asking this question, after all with the constraints you should never have a situation of the sort HNoNils (Hcons EmptyNil l) (HCons EmptyNil l'))
, at least I don't think so.
When adding back OverlappingInstances, I get even weirder errors that I don't understand:
Couldn't match type `True' with `False'
When using functional dependencies to combine
TtEq a a True,
arising from the dependency `a b -> eq'
in the instance declaration at /home/raphael/Dropbox/IST/AFRP/arrow.hs:23:14
TtEq EmptyNil EmptyNil False,
arising from a use of `hNoNils'
at /home/raphael/Dropbox/IST/AFRP/arrow.hs:53:13-19
In the second argument of `($)', namely `hNoNils testList2'
In a stmt of a 'do' block: print $ hNoNils testList2
the second statement, TtEq EmptyNil EmptyNil False
, seems to say that an instance has been generated by a function call...? I am a bit confused as to where it came from.
So in trying to figure this out, I was wondering:
is it possible to get some more verbose information on how Haskell works with instances? Some of these combinations seem impossible. Even just a link to a document explaining the mechanism would be appreciated
Is there a more specific definition to how
OverlappingInstances
work? I feel like I'm missing something (like maybe the "specificity" argument works only with jthe type variables, not with the number of constraints...)
edit: So I tried one of the suggestions of C.A. McCann (removing some of the constraints) to the following:
instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'
instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')
instance HNoNils HNil HNil
Doing this gives me some nasty overlapping instances errors:
Overlapping instances for HNoNils
(HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l')
arising from a use of `hNoNils'
Matching instances:
instance [overlap ok] HNoNils l l' => HNoNils (HCons EmptyNil l) l'
-- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:33:10
instance [overlap ok] HNoNils l l' =>
HNoNils (HCons e l) (HCons e l')
-- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:37:10
I feel as if the resolution method is top down instead of bottom up (where the system would never try to find an instance such as this).
edit 2: By adding a small constraint to the second condition, I got the expected behavior (see McCann's comment on his answer):
-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'
where hNoNils (HCons EmptyNil l) = hNoNils l
-- l gives l' means (HCons e l) gives (HCons e l') for all e
instance (HNoNils l l',r~ HCons e l' ) => HNoNils (HCons e l) r
where hNoNils (HCons e l) = hCons e $ hNoNils l
here the added thing is the r~HCons e l'
constraint on the second instance.