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

[Daniel Peebles]

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> wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> 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
>
>
> - --
> 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/
>
> iEYEARECAAYFAlBcXs4ACgkQvjzICpVvX7b1WQCePiL+SFNj9X+U0V2fnykuatLX
> pIcAn1VDNRiSR18s7UgctdPeNzFgStbi
> =LBGb
> -----END PGP SIGNATURE-----
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120921/889bfc5a/attachment.htm>