Why don't we narrow type arguments more frequently

Learn
#1

So, I found out that the type level machinery to get restricted type arguments is surprinsingly small nowadays :

testA :: OneOf '[Text] Text
testA = "ok"
-- Type error : 
-- • The provided type 
--   Int
--    does not match any of the type in the provided OneOf list 
--   '[Text]
-- • In the expression: 10
--   In an equation for ‘testB’: testB = 10
testB :: OneOf '[Text] Int
testB = 10
-- Type error : 
-- • You provided an empty type list for your OneOf, so nothing will typecheck, your type is equivalent to Void
-- • In the expression: "qsd"
--   In an equation for ‘testC’: testC = "qsd"
testC :: OneOf '[] Int
testC = "qsd"

type OneOf listOfType target = OneOfAccum '[] listOfType target
type family OneOfAccum consumed listOfType target where
    OneOfAccum '[] '[] target =  TypeError ('Text "You provided an empty type list for your OneOf, so nothing will typecheck, your type is equivalent to Void")
    OneOfAccum _ (target : resOfType) target = target
    OneOfAccum currentAcc (v : resOfType) target = OneOfAccum (v : currentAcc) resOfType target
    OneOfAccum allCons '[] target =  TypeError ('Text "The provided type "
        ':$$: 'ShowType target ':$$: 'Text " does not match any of the type in the provided OneOf type list " ':$$: 'ShowType allCons)

I find this quite nice. Of course it’s not perfect, since the type error only comes out when it typechecks and not in type aliases or type signatures for instance but still, it seems good.
Hence my question, why don’t people use more this feature, and is there anything in base (or a widespread library) similar to this OneOf type family ?

#2

Do you have any real world examples of when this would be useful? I can’t remember ever really needing something like this.

#3

I stumbled upon this while thinking of Refactoring proposal on Library name · Issue #8567 · haskell/cabal · GitHub
Admittedly it’s not much of a “need” rather a nice addition.
But I mean, it happens very frequently in my experience to have such a type variable closed under certain assumptions. I’d consider it’s the untagged type level equivalent to sum types at the value level.

More specifically in this example I’d type the cabal library as :

data LibraryMain = LMain
data LibrarySub = LSub UnqualComponentName

-- and : 
library :: Maybe (Library LibraryMain)
subLibraries :: [Library LibrarySub]

-- and : 
data Library libType = Library { libName :: OneOf '[LibraryMain, LibrarySub] libType, etc }
#4

I think I’d do that with GADTs:

data LibType = LibMain | LibSub

type LibName :: LibType -> Type
data LibName a where
  LMain :: LibName LibMain
  LSub :: UnqualComponentName -> LibName LibSub

library :: Maybe (Library LibMain)
subLibraries :: [Library LibSub]

type Library :: LibType -> Type
data Library a = Library { libname :: LibName a, ... }
1 Like
#5

Haha, very nice thanks :slight_smile: . I did try that, but I gave up after trying to use the GADT on the record constructor which felt extremely unfit and required redundancy in fields definition.

I guess that’s an answer then, GADTs should fill most of the requirements for my type family based solution.

PS: A notably better aspect of your solution is that it also fails when simply using the type in a signature when the type argument doesn’t fit.

PS2: Still, why is this design not used more frequently, I feel like most of the time the type level argument is restricted to some types in the signatures and this is not enforced somehow ?