[GHC] #6018: Injective type families
GHC
ghc-devs at haskell.org
Fri Jan 9 21:31:12 UTC 2015
#6018: Injective type families
-------------------------------------+-------------------------------------
Reporter: lunaris | Owner: jstolarek
Type: feature request | Status: new
Priority: normal | Milestone: 7.12.1
Component: Compiler | Version: 7.4.1
Resolution: | Keywords:
Operating System: Unknown/Multiple | TypeFamilies, Injective
Type of failure: None/Unknown | Architecture:
Blocked By: | Unknown/Multiple
Related Tickets: #4259 | Test Case:
| Blocking:
| Differential Revisions: Phab:D202
-------------------------------------+-------------------------------------
Comment (by jberryman):
I'm very late to the discussion, so this is probably not helpful at all,
but I wanted to mention my interest. I've only had use for better type
inference with (conceptually) closed, recursive type families. What I
think I want is something like proposal C from the wiki, or the head-
injectivity proposal where "possibly-partial information about the result
might allow us to deduce possibly-partial information about the
arguments."
And as a naive user I want injectivity to be inferred for closed type
families, and don't find the arguments against it in the wiki convincing.
Intuitively there doesn't seem to be much difference between the level of
logic required to infer things about types with closed type synonym
families, vs the sort of inference the typechecker does elsewhere (again,
as a naive user who doesn't care about the trickiness of implementing such
a scheme). My impression is that this is what many people assumed would be
the point of closed type families; for what I've had in mind closed type
families make only a cosmetic improvement.
Anyway most of my interest came from my work on
https://github.com/jberryman/shapely-data which embarrassingly seems to
dependent quite a lot on #1241, so it (and below) needs GHC 7.6. You can
ignore the example that follows or consider it if it's helpful:
{{{#!hs
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-} -- for nested Type family: Reversed
(Tail t) :> Head t
{-# LANGUAGE FunctionalDependencies #-}
-- | A class for the exponent laws with the 'Normal' form @abc@ in the
exponent
-- place. See the instance documentation for concrete types and examples.
class Exponent abc where
fanin :: (abc :=>-> x) -> (abc -> x)
unfanin :: (abc -> x) -> (abc :=>-> x)
-- | The algebraic normal form 'Exponent' @abc@ distributed over the
single
-- base variable @x at .
type family abc :=>-> x
-- | x¹ = x
type instance () :=>-> x = x
-- | x⁽ᵃᵇ⁾ = (xᵇ)ᵃ
type instance (a,bs) :=>-> x = a -> bs :=>-> x
instance Exponent () where
fanin = const
unfanin f = f ()
instance (Exponent bs)=> Exponent (a,bs) where
fanin f = uncurry (fanin . f)
unfanin f = unfanin . curry f
class Homogeneous a as | as -> a where
-- An n-ary @codiag at .
genericRepeat :: a -> as
instance Homogeneous a () where
genericRepeat _ = ()
instance (Homogeneous a as)=> Homogeneous a (a,as) where
genericRepeat a = (a,genericRepeat a)
}}}
So the following two type-check fine:
{{{#!hs
a = (3 ==) $ (\(x,(y,(z,())))-> x+y+z) $ genericRepeat 1
b = (3 ==) $ fanin (\x y z-> x+y+z) (genericRepeat 1 ::
(Int,(Int,(Int,()))))
}}}
But this doesn't:
{{{#!hs
c = (3 ==) $ fanin (\x y z-> x+y+z) $ genericRepeat 1
}}}
...failing with
{{{
Couldn't match expected type `a1 -> a1 -> a1 -> a1'
with actual type `abc0 :=>-> a0'
The type variables `a0', `abc0', `a1' are ambiguous
Possible fix: add a type signature that fixes these type variable(s)
The lambda expression `\ x y z -> x + y + z' has three arguments,
but its type `abc0 :=>-> a0' has none
In the first argument of `fanin', namely `(\ x y z -> x + y + z)'
In the expression: fanin (\ x y z -> x + y + z)
}}}
That library is probably going in the garbage bin at this point, but in
general this is the sort of thing I think I'd like to be able to do with
type families eventually. And I haven't gotten to dig into y'all's
singletons work yet, so it might be that that's the sort of thing I'm
looking for and my use of type families and classes in shapely-data is
ill-considered.
Thanks for your work on this!
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:103>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list