Re: [GHC] #6018: Injective type families
#6018: Injective type families +--- Reporter: lunaris | Owner: simonpj Type: feature request | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler | Version: 7.4.1 Keywords: TypeFamilies, Injective | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Changes (by conal): * cc: conal@… (added) Comment: Note [http://haskell.1045720.n5.nabble.com/Injective-type-families- td3385084.html this discussion], which includes the subtlety of injective ''in'' various arguments (holding other fixed). -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families +--- Reporter: lunaris | Owner: simonpj Type: feature request | Status: new Priority: normal | Milestone: 7.8.1 Component: Compiler | Version: 7.4.1 Keywords: TypeFamilies, Injective | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Changes (by igloo): * owner: = simonpj * milestone: = 7.8.1 Comment: Simon, I'm no sure what the status of this is, but it looks like your area so I'm assigning it to you. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families +--- Reporter: lunaris | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.4.1 Keywords: TypeFamilies, Injective | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Changes (by nfrisby): * cc: nfrisby (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families +--- Reporter: lunaris | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.4.1 Keywords: TypeFamilies, Injective | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Changes (by nathanhowell): * cc: nathanhowell@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families +--- Reporter: lunaris | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.4.1 Keywords: TypeFamilies, Injective | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Changes (by goldfire): * cc: eir@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families +--- Reporter: lunaris | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.4.1 Keywords: TypeFamilies, Injective | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Changes (by mokus): * cc: mokus@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families
+---
Reporter: lunaris | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Keywords: TypeFamilies, Injective | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby: |Blocking:
Related: |
+---
Comment(by mokus):
An interesting use case is type-level co-naturals using -XDataKinds (which
I'm using as the height type index for an experimental 2^k-tree
implementation):
{{{
data Nat
= Zero
| Suc Nat
data CoNat
= Co Nat
| Infinity
type family Succ (t :: CoNat) :: CoNat
type instance Succ (Co n) = Co (Suc n)
type instance Succ Infinity = Infinity
}}}
Succ can't be a constructor, because then Succ Infinity /~ Infinity. Succ
as a type family half-works, but you end up needing
(logically-)unnecessary type annotations all over the place because GHC
doesn't know that Succ n ~ Succ m = n ~ m. It might be possible to
devise some kind of type-level bisimilarity constraint, but I suspect it
would actually increase the need for type annotations rather than decrease
it.
I've also tried an alternate definition of the tree type using Pred
instead of Succ, but that seems to lead to really bizarre types - it
accepts obviously non-flat trees at a type indicating that the tree's
height is zero (or actually, any CoNat I want), because it accepts the
existence of types such as Pred (Co Zero). Is this expected behavior
(e.g., due to the open-world assumption) or should I file a bug report on
that?
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:5
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families
+---
Reporter: lunaris | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Keywords: TypeFamilies, Injective | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby: |Blocking:
Related: |
+---
Changes (by simonpj):
* difficulty: = Unknown
Comment:
Some functions might be injective in one argument but not another. For
example:
{{{
F a b ~ F c d ===a ~ c
but not b ~ d
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families +--- Reporter: lunaris | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.4.1 Keywords: TypeFamilies, Injective | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Comment(by lunaris): Indeed; I'd not considered that case. I'm not aware of a well-defined semantics for injective type functions in the context of constraint solving so I've no idea how to proceed. There are of course syntactic complications also. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
[GHC] #6018: Injective type families
#6018: Injective type families
--+-
Reporter: lunaris | Owner:
Type: feature request | Status: new
Priority: normal| Component: Compiler
Version: 7.4.1 | Keywords: TypeFamilies, Injective
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby:| Blocking:
Related:|
--+-
Injective type families have been discussed several times on the mailing
list and identified as a potentially useful feature.
I've naively attempted a proof-of-concept in GHC. It's almost certainly
incorrect and probably breaks the type system, but I thought it best to
put it here and see if it can be made workable.
In summary, my changes are:
* Add a new keyword, {{{injective}}}, which is available only when the
{{{TypeFamilies}}} extension is enabled. Injective families may then be
defined thus:
{{{
injective family F a :: *
type instance F Int = Bool
type instance F Bool = Int
injective family G a :: *
type instance G a = a
}}}
Syntax is of course completely changeable; I've simply picked one of the
possible designs. Hopefully this won't be subjected to too much bike-
shedding.
* Add the constructor {{{InjFamilyTyCon}}} to {{{TyConRhs}}} and the
family flavour {{{InjectiveFamily}}} to {{{HsSyn}}}. Again, I've opted to
encode injectivity as a flavour rather than (say) a {{{Bool}}} attached to
type families. This is a completely arbitrary choice and may be utterly
stupid.
* Altered the definition of decomposable {{{TyCon}}}s to include
injective families ({{{isDecomposableTyCon}}}). This effectively
introduces a typing rule that says if we have {{{(F a ~ F b)}}} then we
can deduce {{{(a ~ b)}}} ({{{TcCanonical}}}).
* Modified the unifier so that it will attempt to replace saturated
injective families with their left-hand sides where possible
({{{TcUnify}}}). This means that in a function such as:
{{{
f :: F a - F a
f = ...
}}}
The type of {{{f False}}} is inferred as {{{F Int}}} (i.e., {{{a}}} is
no longer ambiguous).
Some things work, some things don't. For example, the attached file
typechecks, but if I actually try to evaluate {{{f False}}} I get nothing
(not even a Segmentation fault).
See what you think.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6018: Injective type families
#6018: Injective type families
--+-
Reporter: lunaris | Owner:
Type: feature request | Status: new
Priority: normal| Component: Compiler
Version: 7.4.1 | Keywords: TypeFamilies, Injective
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby:| Blocking:
Related:|
--+-
Comment(by lunaris):
Oops -- I forgot to list all that was wrong with the current
implementation. Namely:
* In the example, {{{g}}}'s type is inferred as {{{a - a}}} (and not
{{{G a - G a}}}). This is in some sense `correct', but seems a bit dodgy.
* I don't actually *enforce* that the declared instances of a family
*are* injective yet -- I've put that off until what's there is semi-
stable.
* I've messed up and inadvertently included whitespace changes in one of
the patches. Apologies.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6018#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
