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

-----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 mailto:florian.lorenzen@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@haskell.org mailto:Haskell-Cafe@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@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-----