Fix type-level indexed STLC

goldfirere commented 8 years ago

See here:

https://gist.github.com/AndrasKovacs/c7d385aa117929503feb

AndrasKovacs commented 8 years ago

(The code in the linked gist isn't edifying anymore, since now it works as intended).

Is it alright if I dump here my bugs and feature requests? I apologize in advance if it's not. I realize GHC trac is a better outlet for this, it's just that I'm lazy and not yet familiar with trac and I think most of the following should be relevant for you anyway. It might also be the case that I misinterpreted some things that are by design as bugs.

Bug 1:

import GHC.Prim

type Foo a = Any

This is fine with GHC 7.10.2, but gets me the following funny message with HEAD:

Notes.hs:6:1: error: …
    • The type family ‘Any’ should have no arguments, but has been given none
    • In the type synonym declaration for ‘Foo’
Compilation failed.

Bug 2:

{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies #-}
import Data.Kind

data TyFun a b
type a ~> b = TyFun a b -> Type -- I love this
type family (@@) (f :: a ~> b) (x :: a) :: b

infixr 0 ~> 
infixl 9 @@

type family If
  (p :: Bool ~> Type) (t :: p @@ True) (f :: p @@ False) (b :: Bool) :: p @@ b where
  If p t f True  = t
  If p t f False = f

This gives errors on both equations in If. The error for the True case is:

Notes.hs:13:20: error:
    • Expected kind ‘p1 @@ 'True’, but ‘t’ has kind ‘p @@ 'True’
    • In the type ‘t’
      In the type family declaration for ‘If’

It works though with plain old type constructors as induction motive:

type family If'
  (p :: Bool -> Type) (t :: p True) (f :: p False) (b :: Bool) :: p b where
  If' p t f True = t
  If' p t f False = f

Bug 3:

{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies #-}
import Data.Kind
import Data.Proxy

type family Not (b :: Bool) :: Bool where
  Not True  = False
  Not False = True

type family Foo (b :: Bool) (p :: Proxy (Not b)) :: Type where
  Foo b 'Proxy = ()

This throws:

Notes.hs:10:3: error:
    • Illegal type synonym family application in instance: 'Proxy
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

The error message goes away if I instead write Foo b p = (). I get a different error though (similar to bug no. 2) if I write Foo b ('Proxy :: Proxy (Not b)) = ():

Notes.hs:10:9: error: …
    • Expected kind ‘Proxy (Not b)’,
        but ‘'Proxy’ has kind ‘Proxy (Not b1)’
    • In the second argument of ‘Foo’, namely
        ‘(Proxy :: Proxy (Not b))’
      In the type family declaration for ‘Foo’
Compilation failed.

Bug 4:

{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies, GADTs #-}

import Data.Kind

type family Const a b where
  Const a b = a

data Bar (b :: Bool) :: Const Type b

This throws Kind signature on data type declaration has non-* return kind. This isn't an important or severe issue, but I think it'd make sense to first normalize the return type.

Misc:

With the STLC in my gist, if I do :kind! Eval Mul @@ S (S Z) @@ S (S Z), it takes 13 second to print the answer with my i7 3770 CPU. It might be worthwhile to investigate this rather heavy slowdown.
I think we should be able to use type families in instance heads. Currently it's always an error, even if a type family would immediately reduce to a a valid instance head.
Symbol has limited use as it is. I tried to implement STLC with Symbol variables, but I quickly ran into the problem that Symbol doesn't have any type-level decidable equality, and it can't be implemented by a programmer either. We can't really compute on it too, because each Symbol is an opaque blob. It would be good if we had at least concatenation and decidable equality, but type Symbol = [Char] would be better IMO.
I tried to hack together semi-decidable Symbol equality using non-linear type family patterns and Any, but I found that there's no type-level analogue of unsafeCoerce. We can implement Coerce (a == b) (x :: a) :: b with Any as a bogus equality proof, but the resulting expression doesn't reduce, and thus the coerced value can't be used anywhere. I realize though that a true unsafeCoerce on the type level may be unacceptably dangerous.

goldfirere commented 8 years ago

This is very helpful! Thanks. And, yes, please do post things like this. I certainly do.

Bug 1 is pretty terrible. I'll see if I can take a look soon, as the output is embarrassing and my hunch is that the fix is quick.

Type families with arguments that mention kind families in their kinds are completely broken right now, as you've observed. I know how to fix this but have yet to implement the fix.

Normalizing that result kind is harder than you might think. I'll save that one for later, I think.

Ick. 13 seconds to reduce. I have a very strong hunch this is related to the slowdowns in some of our performance tests. But perhaps your test case is simpler. I'll look at it when I sweep up the performance bugs.

Type families in instance heads have been suggested before. But I think it's a step in the wrong direction, rather like allowing f (not True) = 5 at the term level. not True immediately reduces to False, so this is sensible, for a sufficiently lax definition of sensible. But that doesn't make it a good idea. Somehow, in types, it feels more sensible (even to me). I remain very far from convinced that this is a good idea though.

Why doesn't Symbol have decidable equality? Doesn't CmpSymbol work? And type family a == b where a == a = True; a == b = False should also work.

Concatenation and decomposition of Symbols would be lovely. But once we start down that road, we'll want GHC to be able to reason about splitting and splicing operations, and it doesn't do that. I think once we figure out the right way to strap an SMT solver to GHC's type-checker, there will be more action on this front. In the meantime, it's quite easy to write a quasiquoter that turns strings into type-level lists of characters (that is, one-character Symbols). These are ugly, but they get the job done. In any case, I personally don't have any plans to improve this in the near future, I'm afraid.

It would be straightforward to add UnsafeCoerce at the type level, and it would indeed reduce. (Straightforward within GHC, that is.) And it's actually safer than unsafeCoerce in expressions. Indeed, I tend to think UnsafeCoerce, by itself, wouldn't allow you to write unsafeCoerce. It wouldn't shock me if I'm wrong. I'll see if I can slip this in -- I like it.

AndrasKovacs commented 8 years ago

As to Symbol, it seems I remembered my issues wrong. Pattern matching and CmpSymbol do work for equality.

goldfirere / ghc