Shouldn't you have<div><br></div><div>IxZero :: Ix (CtxCons ty ctx) ty</div><div><br></div><div>instead of</div><div><br></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)">IxZero :: Ix ctx ty</span><br>
<br><br><div class="gmail_quote">On Fri, Sep 21, 2012 at 8:34 AM, Florian Lorenzen <span dir="ltr"><<a href="mailto:florian.lorenzen@tu-berlin.de" target="_blank">florian.lorenzen@tu-berlin.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">-----BEGIN PGP SIGNED MESSAGE-----<br>
Hash: SHA1<br>
<br>
Hello cafe,<br>
<br>
I have the following GADT definitions capturing the simply typed<br>
lambda calculus with de Bruijn indices for variables and explicitly<br>
annotated types for variables:<br>
<br>
<br>
{-# LANGUAGE GADTs #-}<br>
{-# LANGUAGE KindSignatures #-}<br>
{-# LANGUAGE DataKinds #-}<br>
<br>
- -- Typing contexts<br>
data Ctx = CtxNil<br>
| CtxCons Ctx Type<br>
<br>
- -- Types<br>
data Type = TyInt<br>
| TyArrow Type Type<br>
<br>
- -- Variable indices<br>
data Ix (ctx :: Ctx) (ty :: Type) where<br>
IxZero :: Ix ctx ty<br>
IxSucc :: Ix ctx ty1 -> Ix (CtxCons ctx ty2) ty1<br>
<br>
- -- Type representations<br>
data TyRep (ty :: Type) where<br>
TyRepInt :: TyRep TyInt<br>
TyRepArrow :: TyRep ty1 -> TyRep ty2 -> TyRep (TyArrow ty1 ty2)<br>
<br>
- -- Terms<br>
data Term (ctx :: Ctx) (ty :: Type) where<br>
TmInt :: Integer -> Term ctx TyInt<br>
TmVar :: Ix ctx ty -> Term ctx ty<br>
TmAdd :: Term ctx TyInt -> Term ctx TyInt -> Term ctx TyInt<br>
TmApp :: Term ctx (TyArrow ty1 ty2) -> Term ctx ty1 -> Term ctx ty2<br>
TmAbs :: TyRep ty1 -> Term (CtxCons ctx ty1) ty2<br>
-> Term ctx (TyArrow ty1 ty2)<br>
<br>
For the following definition<br>
<br>
test1 = TmAbs TyRepInt (TmVar IxZero)<br>
<br>
GHCi infers the type<br>
<br>
test1 :: Term ctx (TyArrow 'TyInt ty2)<br>
<br>
I was a bit puzzled because I expected<br>
<br>
Term ctx (TyArrow TyInt TyInt)<br>
<br>
Of course, this more special type is an instance of the inferred one,<br>
so I can assign it by a type signature.<br>
<br>
Can someone explain why the inferred type is more general?<br>
<br>
Terms like<br>
<br>
test2 = TmAbs TyRepInt (TmAdd (TmVar IxZero) (TmInt 5))<br>
<br>
have the type I expected:<br>
<br>
test2 :: Term ctx (TyArrow 'TyInt 'TyInt)<br>
<br>
<br>
Thank you and best regards,<br>
<br>
Florian<br>
<br>
<br>
- --<br>
Florian Lorenzen<br>
<br>
Technische Universität Berlin<br>
Fakultät IV - Elektrotechnik und Informatik<br>
Übersetzerbau und Programmiersprachen<br>
<br>
Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin<br>
<br>
Tel.: +49 (30) 314-24618<br>
E-Mail: <a href="mailto:florian.lorenzen@tu-berlin.de">florian.lorenzen@tu-berlin.de</a><br>
WWW: <a href="http://www.user.tu-berlin.de/florenz/" target="_blank">http://www.user.tu-berlin.de/florenz/</a><br>
-----BEGIN PGP SIGNATURE-----<br>
Version: GnuPG v1.4.11 (GNU/Linux)<br>
Comment: Using GnuPG with Mozilla - <a href="http://www.enigmail.net/" target="_blank">http://www.enigmail.net/</a><br>
<br>
iEYEARECAAYFAlBcXs4ACgkQvjzICpVvX7b1WQCePiL+SFNj9X+U0V2fnykuatLX<br>
pIcAn1VDNRiSR18s7UgctdPeNzFgStbi<br>
=LBGb<br>
-----END PGP SIGNATURE-----<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div>