Try translating into System FC! It’s not just a question of what the type
checker will pass; we also have to produce a well-typed FC program.
Remember that (putting in all the kind abstractions and applications:
Thrist :: forall i. ((i,i) -> *) -> (i,i) -> *
(:*) :: forall i j k. forall (a: (i,j) -> *).
a '(i,j) -> Thrist (j,k) a '(j,k) -> Thrist (i,k) a '(i,k)
So consider ‘irt’:
irt :: forall i. forall (a : (i,i) -> *). forall (x : (i,i)).
a x -> Thrist i a x
irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).
(:*) ? ? ? ? ax (Nil ...)
So, what are the three kind args, and the type arg, to (:*)?
It doesn’t seem to make sense... in the body of irt, (:*) produces a result of
type
Thrist (i,k) a ‘(i,k)
but irt’s signature claims to produce a result of type
Thrist i a x
So irt’s signature is more polymorphic than its body.
If we give irt a less polymorphic type signature, all is well
irt :: forall p,q. forall (a : ((p,q),(p,q)) -> *). forall (x : ((p,q),(p,q))).
a x -> Thrist (p,q) a x
Maybe you can explain what you want in System FC? Type inference and the
surface language come after that. If it can’t be expressed in FC it’s out of
court. Of course we can always beef up System FC.
I’m copying Stephanie and Conor who may have light to shed.
Simon
From: Edward Kmett [mailto:ekm...@gmail.com]
Sent: 31 August 2012 18:27
To: Simon Peyton-Jones
Cc: glasgow-haskell-users@haskell.org<mailto:glasgow-haskell-users@haskell.org>
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional
dependency?
It is both perfectly reasonable and unfortunately useless. :(
The problem is that the "more polymorphic" type isn't any more polymorphic,
since (ideally) the product kind (a,b) is only inhabited by things of the form
'(x,y).
The product kind has a single constructor. But there is no way to express this
at present that is safe.
As it stands, I can fake this to an extent in one direction, by writing
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, TypeFamilies,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
module Kmett where
type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a
type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Nil :: Thrist a '(i,i)
(:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>
a ij -> Thrist a '(j,k) -> Thrist a ik
irt :: a x -> Thrist a x
irt ax = ax :- Nil
and this compiles, but it just pushes the problem down the road, because with
that I can show that given ij :: (x,y), I can build up a tuple '(Fst ij, Snd
ij) :: (x,y)
But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later when
you go to define an indexed bind, and type families are insufficient to the
task. Right now to get this property I'm forced to fake it with unsafeCoerce.
-Edward
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
