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@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@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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe