[Haskell-cafe] Question about type inference of a GADT term

[Florian Lorenzen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Yes, of course! Stupid me, thanks for pointing that out Daniel.

Now it works as expected.

Florian

On 09/22/2012 12:55 AM, Daniel Peebles wrote:
> Shouldn't you have
> 
> IxZero :: Ix (CtxCons ty ctx) ty
> 
> instead of
> 
> IxZero :: Ix ctx ty
> 
> 
> On Fri, Sep 21, 2012 at 8:34 AM, Florian Lorenzen 
> <florian.lorenzen at tu-berlin.de
> <mailto:florian.lorenzen at tu-berlin.de>> wrote:
> 
> Hello cafe,
> 
> I have the following GADT definitions capturing the simply typed 
> lambda calculus with de Bruijn indices for variables and
> explicitly annotated types for variables:
> 
> 
> {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE
> DataKinds #-}
> 
> -- Typing contexts data Ctx = CtxNil | CtxCons Ctx Type
> 
> -- Types data Type = TyInt | TyArrow Type Type
> 
> -- Variable indices data Ix (ctx :: Ctx) (ty :: Type) where IxZero
> :: Ix ctx ty IxSucc :: Ix ctx ty1 -> Ix (CtxCons ctx ty2) ty1
> 
> -- Type representations data TyRep (ty :: Type) where TyRepInt ::
> TyRep TyInt TyRepArrow :: TyRep ty1 -> TyRep ty2 -> TyRep (TyArrow
> ty1 ty2)
> 
> -- Terms data Term (ctx :: Ctx) (ty :: Type) where TmInt :: Integer
> -> Term ctx TyInt TmVar :: Ix ctx ty -> Term ctx ty TmAdd :: Term
> ctx TyInt -> Term ctx TyInt -> Term ctx TyInt TmApp :: Term ctx
> (TyArrow ty1 ty2) -> Term ctx ty1 -> Term ctx ty2 TmAbs :: TyRep
> ty1 -> Term (CtxCons ctx ty1) ty2 -> Term ctx (TyArrow ty1 ty2)
> 
> For the following definition
> 
> test1 = TmAbs TyRepInt (TmVar IxZero)
> 
> GHCi infers the type
> 
> test1 :: Term ctx (TyArrow 'TyInt ty2)
> 
> I was a bit puzzled because I expected
> 
> Term ctx (TyArrow TyInt TyInt)
> 
> Of course, this more special type is an instance of the inferred
> one, so I can assign it by a type signature.
> 
> Can someone explain why the inferred type is more general?
> 
> Terms like
> 
> test2 = TmAbs TyRepInt (TmAdd (TmVar IxZero) (TmInt 5))
> 
> have the type I expected:
> 
> test2 :: Term ctx (TyArrow 'TyInt 'TyInt)
> 
> 
> Thank you and best regards,
> 
> Florian
> 
> 
> 
> _______________________________________________ Haskell-Cafe
> mailing list Haskell-Cafe at haskell.org
> <mailto:Haskell-Cafe at haskell.org> 
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
> 

- -- 
Florian Lorenzen

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin

Tel.:   +49 (30) 314-24618
E-Mail: florian.lorenzen at tu-berlin.de
WWW:    http://www.user.tu-berlin.de/florenz/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://www.enigmail.net/

iEYEARECAAYFAlBdktYACgkQvjzICpVvX7ZskwCgnJC9VaIkoWHuTZoP8kGg70Tb
MFsAn0yuBDClSxe32ZTO8pZzz1xOpI2T
=EoV6
-----END PGP SIGNATURE-----