#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by augustss): I don't think a warning is right, I think it's an error. I view closed type families as functions on types, and when you use a function you expect it to reduce to a normal form. With a warning you're saying that T x is sometimes equal to some other type and sometimes it's a new type. That makes no sense to me. It has nothing to do with being inhabited, uninhabited types are perfectly fine. It like saying that if I define a function 'f False = ()' and then do 'print (f True)' it would print "f True", i.e., elevating the function symbol f from a function to a constructor just because it's partial. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dreixel): I don't see why `T Bool` is "not a type". If you really want something like that, you should index `T` over a closed kind: {{{ {-# LANGUAGE DataKinds, TypeFamilies #-} data Un = TInt type family T (a :: Un) :: * where T TInt = () }}} Now it's clear that `T Bool` is indeed not a type, and gives rise to a kind error. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): For what it's worth, I don't have a strong opinion either way. I think we are agreed that: * In an user-written type signature, * if an application of a closed type family is "apart" from all equations of the family, * then we should signal either an error or a warning. Lennart says "error", Richard says "warning", and I can't work up much excitement about which is chosen. One advantage of "error" is that you don't have to add a flag to suppress the warning! Anyway, if someone wants to implement it, go ahead! This all applies to ''user-written type signatures''. I don't want to apply this to "types that appear during the type inference process" because I don't know exactly what that might mean. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): So, to be concrete, if I write: {{{ foo :: Either (T a) a -> a foo (Right x) = x }}} then you would like `(foo (Right True))` to signal a type error. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): It is a weird beast. But I have learned, painfully, that not being able to write down typing judgements is a Bad Sign. It suggests that we don't know exactly which programs should be erroneous and which should be OK. And if we don't know, it's hard to explain to the user which programs are ok and which are not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by augustss): To me saying that `T Bool` is OK because it's inaccessible is akin to saying that type incorrect expressions are OK as long as they are inaccessible. After all, if you don't use them, they can't cause any harm. But for expressions we have decided that this isn't acceptable. I guess making `T a` behave would require something like kind classes. We don't say that the expression `show x` is unconditionally type correct. It depends on the type of `x` belonging to the `Show` class. In the same way, `T a` is not unconditionally type correct, it's only type correct if `a` is one of the types where `T` is well defined. Until we have something like that I think you'll have to accept that the substitution lemma doesn't work. You can pretend it works by saying `T Bool` is a type, if that makes you happier. I just wonder which type it is. :) But I'm not asking for the moon. :) I'd just like the compiler to tell me when it finds something that is clearly not going to work, like `T Bool`. Exactly under what conditions and how it tells me, I don't care. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:12 augustss]:

To me saying that `T Bool` is OK because it's inaccessible is akin to saying that type incorrect expressions are OK as long as they are inaccessible. After all, if you don't use them, they can't cause any harm. But for expressions we have decided that this isn't acceptable.

I actually would say that an inaccessible expression is ''always'' type- correct, because inaccessibility means that there is a proof of ''false'' in the context, and thus anything is possible. But that's perhaps a story for another day.

I guess making `T a` behave would require something like kind classes.

It's a little worse than that, I think. Say `x :: Z`. In `show x`, we know `Z` must be in the `Show` class, and we also know that ''anything'' of type `Z` is a valid parameter to `show`. Thus, we have substitution, because substitution preserves types. But, in closed type families, we have a stranger situation: `T a` where `a :: *` is acceptable, but `T Bool` is not. I think kind classes (which can be kludged today) don't solve this problem.

But I'm not asking for the moon. :) I'd just like the compiler to tell me when it finds something that is clearly not going to work, like `T Bool`. Exactly under what conditions and how it tells me, I don't care.

This is certainly possible. It's just that the behavior around this feature won't be complete and might not be predictable in corner cases. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by augustss): Replying to [comment:13 rwbarton]:

Isn't it analogous to saying that incomplete pattern matches are OK as long as they are inaccessible? (Which they are.) After all, like you said, a closed type family is like a function on types. The type expression `T Bool` has no normal form, for sure, but who says we have to evaluate it?

Yes, it's a lot like a pattern match failure. So let us go with that analogy for a moment. Assume we have these definitions: {{{#!hs foo :: Int -> Int foo 0 = 42 bar = foo 5 - foo 5 }}} Since we know that `x - x = 0` it is tempting to optimize the definition of `bar` to `bar = 0`. This is, of course, wrong since computing `foo 5` will result in bottom. Now compare this to what the type checker does in my original example. It happily assumes that `T Bool` is equal to `T Bool`, but that's wrong. `T Bool` is bottom at type checking time and should be reported as such. I've decided I'm OK with having `T Bool` just floating around in the same way that I'm OK with having `foo 5` floating around in a lazy language. Type families introduce partial functions on the type level, and I think this has to be dealt with. Type expressions can now blow up during type checking. So at the points when a (closed) type family expression has to be evaluated, e.g., for equality comparison, and it cannot be reduced then this should be an error. IMHO. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by augustss): Replying to [comment:17 goldfire]:

Unfortunately, this, too, violates the substitution lemma. We probably want to be able to solve `(a ~ a)` with reflexivity, for ''any'' `a`. But, you're suggesting that a particular value for `a`, namely `T Bool`, will ''not'' equal itself.

I'm saying it's neither equal to itself, nor unequal to itself. `T Bool` is in some sense ill formed, so asking if it's equal to itself is nonsensical, because it's not a a type. Can you use reflexivity to conclude `Int Bool ~ Int Bool`? No, because it's an ill-formed typed. The case with `T Bool` is not as severely ill form, though. If you want to keep `T Bool` you have to have a different explanation what makes a type. Types a made from `data`, `newtype`, and `type family`. But for `type family` certain of the the types are actually equal to other existing types. But if no equation holds then it's a new (empty) type, distinct from all other types. I can go along with that explanation, but it's not very satisfactory to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Lennart, I don't understand comment:19 at all. Can you give an example to illustrate what you mean? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) Comment: Type families as currently implemented really are axiomatically-defined functional relations: we don't have an operational semantics for them as functions. I agree that being able to write actual functional programs at the type level would be nice, but we can't yet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by jstolarek): Adam, you meant Phab:D841, not Phab:D481. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by DerekElkins): This is a fun one. We can look at what some other systems do in similar situations. comment:17 talks about handling unevaluated terms and the discussion has been talking about partial functions. One system that deals in this realm is Computational Type Theory (CTT), the type theory underlying NuPRL (and now JonPRL). In NuPRL you can literally write the equivalent of: {{{#!hs T Int = Bool T x = fix id }}} Obviously NuPRL doesn't loop forever when it encounters T Bool. It will do some computation to see if it can decide the proposition, but if it can't it gives up and makes it a proof obligation that the user must discharge. Since CTT is based on partial equivalence relations, T Bool ~ T Bool presents no problem. Reflexivity is not given, so that's a statement that needs to be proven. Indeed, typing Lennart's f from the bug report, requires, as usual, deriving that T Bool :: * and in CTT this is by definition T Bool ~ T Bool. Clearly GHC has evidence allowing it to automatically show the proof obligation is not achievable in this case. Thus the analogous situation in CTT would be a type error. In comment:19 Lennart mentions that we still have logic programming at the type level. One way of interpreting this is to give (closed) type families Curry's semantics, i.e. narrowing, but restricted to functional relations, so no (truly) overlapping patterns. This would be a language where a function returns at most one result rather than exactly one result as in a functional language. Still, T Bool would narrow the result set to the empty set and thus be a type error. Alternatively, Lennart may have just been referring to working with uninterpreted functions, something commonly done in logic programming, but in no way restricted to logic programming. Of course, T isn't an uninterpreted function, T Int ~ Bool. We could say it's a quotient of a type of uninterpreted functions modulo the relation T Int ~ Bool. We can push this idea a little. If someone wants to play with the current behavior in a more explicit manner all one needs to do is open up Agda and type: {{{#!hs import Level data Unit : Set where U : Unit data Bool : Set where True : Bool; False : Bool data _==_ {l}{A : Set l} (a : A) : A -> Set l where refl : a == a subst : {l : Level.Level}{A B : Set l} -> (A == B) -> A -> B subst refl x = x postulate T : Set -> Set postulate T_Bool_is_Unit : T Bool == Unit f : T Unit -> Bool f _ = True g : T Bool -> Unit g x = subst T_Bool_is_Unit x h : T Bool == T Bool -> Unit h refl = U }}} To handle overlapping, explicit inequality evidence needs to be provided. This suggests that like we can view a data declaration as adding a constructor to (codes for) *. A type family could be viewed into making that data type a higher inductive type (from Homotopy Type Theory). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by jonsterling): Replying to [comment:26 DerekElkins]:

This is a fun one. We can look at what some other systems do in similar situations.

comment:17 talks about handling unevaluated terms and the discussion has been talking about partial functions. One system that deals in this realm is Computational Type Theory (CTT), the type theory underlying NuPRL (and now JonPRL). In NuPRL you can literally write the equivalent of:

{{{#!hs T Int = Bool T x = fix id }}}

thanks for the shoutout! I just thought I would clarify that, whilst in the past it was considered and perhaps experimented with, Nuprl does not currently have the ability to perform case analysis on types. (However, one of the principle reasons for types having an intensional equality in Nuprl rather than the standard extensional one is to not rule out the option of providing an eliminator to the universe in the future.) Anyway—with regard to partial operations, you are correct that it is not really a problem in Nuprl or JonPRL if a definition is partial; reduction is guided by the user in Nuprl. (By the way, contrary to oft-repeated mythology, it *is* safe to reduce terms in any context in CTT/ETT—this is guaranteed by the fact that computational equivalence is a congruence, a well-known result that comes from Howe.) It is *not* the case that for some function `f` and value `m`, `f(m)` is stuck (or worse, "canonical") if `f` is not defined at `m`; instead, it diverges. So viewing Haskell-style type families (whether open or closed) as functions or operations doesn't really work, though I believe that in many cases where a Haskell programmer reaches for a type family, they are really wanting a function/operation. I like your view of type families as generative in the same sense as data families, but quotiented by further axioms. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler