Serokell’s Work on GHC: Dependent Types, Part 5

Links
1
49 Likes
2

This is great. I love this work!

2 Likes
3

Dependent Haskell is what allows me to confidently focus my efforts on Haskell. IMO, it will allow Haskell to maintain a clear advantage over other languages for the foreseeable future.

My sincerest thanks to all of the brilliant people doing this work! Thanks for striving ever-onward toward making this a language with which we can achieve most anything within possibility.

Ps. I was listening to the Haskell cast the other day and heard Eisenberg say that if DT doesn’t land by 2017, it would be “late”. Oh you sweet summer child. :grin: Isn’t that always the way?!? Anyway, thanks again to everyone involved and special thanks to Jesse for doing the hard initial work toward this goal.

6 Likes
4

About the Tuple type family. In Tuple (Int, Bool), does the (Int, Bool) have kind Tuple2 Type Type?

5

Correct!

  • If your module is compiled with NoListTuplePuns, then (Int, Bool) :: Tuple2 Type Type, and the Tuple type family maps it to Tuple2 Int Bool. That’s the intended usage.

  • But that’s not all. If you compile with ListTuplePuns, then (Int, Bool) :: Type, because it already is Tuple2 Int Bool, and then applying Tuple is identity.

So the Tuple type family works regardless of (No)ListTuplePuns. Now that I’ve spelled this out, it’s also occurred to me that this means Tuple is idempotent, i.e. forall x. Tuple (Tuple x) = Tuple x.

8 Likes
6

Thank you Vladislav.

Good to hear you could rescue the StarIsType syntax. TIL (*) → (*) is also a valid kind. That looks even more like an operator section.

Might kind signatures turn up in patterns in future work? Is there a risk of confusing the kind -> with a ViewPattern?

1 Like
7

-- Expressions
t1 = Typed Int 42
t2 = Typed String “hello”
t3 = Typed (Int → Bool) even

I’m so used to putting the type following the expr, this still doesn’t feel right (even though I knew it was coming). Is it really not possible to support

t1’ = Typed 42 (type Int)

  Typed :: forall a. a → (type a) → T a

Addit: To answer my own q, I tried flip Typed 42 (type Int). Rejected as an argument to flip, because of a type mismatch. So RequiredTypeArguments are second-class. This rather breaks my mental model of ‘argument’ for a lambda-calculus inspired language.

8

I’m surprised/disappointed. This gets rejected:

t42 = Typed (type Int) 42

    Unexpected keyword `type’
    Suggested fix: … `ExplicitNamespaces’ … (implied by …)

If there’s anything that implies that extension, surely it would be RequiredTypeArguments(?) I particularly remember that stipulation in the discussion.

9

  • The flip situation is indeed rather disappointing. For reference, Agda’s type for flip looks like this:

    flip : ∀ {A : Set a} {B : Set b} {C : A → B → Set c} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y

    And it relies on higher-order unification to instantiate C at use sites. It’s not clear to me what the Haskell solution to this problem could be.

  • The ExplicitNamespaces problem is easier to address. Making one extension imply another is a one-line change, from the implementation standpoint.

2 Likes
10

Yes. Tried initially in 9.10 with no extensions

ghci> let f ((+ 2) -> x) = x in f 7
    Illegal view pattern; suggest enable the extension [correct, same reporting as prev GHCs]

— instead :set -XRequiredTypeArguments; try same input
    error: [GHC-72516] Parse error in pattern: +2

— Ok, :set -XViewPatterns; parsed ok.
— BTW, advance warning:

ghci> let f ((+ 2) -> x :: Int) = x in f 7
    warning: [GHC-00834] …
    * Found an unparenthesized pattern signature …
    * This code might stop working in a future GHC release …

(I was trying to break it :: I wouldn’t usually code that signature like that — yeuch! So I agree with the planned change to the precedence.)