[Haskell-cafe] Transforming a ADT to a GADT

[José Pedro Magalhães]

Hi Florian,

Will this do?

class Tc a where
  tc :: Exp -> Maybe (Term a)

instance Tc Int where
  tc (Lit i)      = return (TLit i)
  tc (Succ i)     = tc i >>= return . TSucc
  tc (IsZero i)   = Nothing
  tc e            = tcIf e

instance Tc Bool where
  tc (Lit i)      = Nothing
  tc (Succ i)     = Nothing
  tc (IsZero i)   = tc i >>= return . TIsZero
  tc e            = tcIf e

tcIf :: (Tc a) => Exp -> Maybe (Term a)
tcIf (If c e1 e2) = do c' <- tc c
                       e1' <- tc e1
                       e2' <- tc e2
                       return (TIf c' e1' e2')


Cheers,
Pedro

On Fri, Sep 14, 2012 at 11:45 AM, Florian Lorenzen <
florian.lorenzen at tu-berlin.de> wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Hello cafe,
>
> I have a question wrt. to GADTs and type families in GHC (7.6.1).
>
> I'd like to transform a value of an ADT to a GADT. Suppose I have the
> simple expression language
>
> > data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp
>
> and the GADT
>
> > data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int ->
> Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term
> ty -> Term ty -> Term ty
>
> that encodes the typing rules.
>
> Now, I'd like to have a function
>
> > typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>
>
> that returns the GADT value corresponding to `exp' if `exp' is type
> correct.
>
> I found a solution at
> http://okmij.org/ftp/tagless-final/TypecheckedDSLTH.hs but this has as
> type (slightly adapted)
>
> > typecheck :: Exp -> Maybe TypedTerm
>
> with
>
> > data TypedTerm = forall ty. (Typ ty) (Term ty) > data Typ ty =
> > TInt
> Int | TBool Bool
>
> That is, the GADT value is hidden inside the existential and cannot be
> unpacked. Therefore, I cannot write a type preserving transformation
> function like
>
> > transform :: Term t -> Term t
>
> that gets the result of the `typecheck' function as input.
>
> The solution mentioned above uses Template Haskell to extract the
> `Term t' type from the existential package and argues that type errors
> cannot occur during splicing.
>
> Is there a possibility to avoid the existential and hence Template
> Haskell?
>
> Of course, the result type of typecheck depends on the type and type
> correctness of its input.
>
> My idea was to express this dependency by parameterizing `Exp' and
> using a type family `ExpType' like:
>
> > typecheck :: Exp e -> Maybe (Term (ExpType e)) > typecheck (ELit
> > i)
> = Just (TLit i) > typecheck (ESucc exp1) = case typecheck exp1 of >
> Nothing -> Nothing > Just t -> Just (TSucc t) > <...>
>
> with
>
> > data TEXP = L | S TEXP | IZ TEXP | I TEXP TEXP TEXP -- datakind >
> > >
> data Exp (e::TEXP) where > ELit :: Int -> Exp L > ESucc :: Exp e1 ->
> Exp (S e1) > EIsZero :: Exp e1 -> Exp (IZ e1) > EIf :: Exp e1 -> Exp
> e2 -> Exp e3 -> Exp (I e1 e2 e3)
>
> It seems to me that `ExpType' then would be a reification of the type
> checker for `Exp' at the type level. But I did not know how to define
> it. Does it make sense at all? Is it possible in GHC?
>
> All the examples on the net I looked at either start with the GADT
> right away or use Template Haskell at some point. So, perhaps this
> `typecheck' function is not possible to write in GHC Haskell.
>
> I very much appreciate any hints and explanations on this.
>
> 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/
>
> iEYEARECAAYFAlBTCr8ACgkQvjzICpVvX7ZfTgCeOPflPtaEW/w1McjYWheaRaqq
> oUQAnRXSrGP3se+3oiI3nnd+B/rK8yx8
> =X1hR
> -----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/20120916/9f13deec/attachment.htm>