[Haskell-cafe] Transforming a ADT to a GADT

[Florian Lorenzen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

José, it occurs to me that with this solution, I always have to
prescribe the type as in

> tc (Succ (Lit 5)) :: Maybe (Term Int)

Otherwise, I obtain the message

Ambiguous type variable `a0' in the constraint:
      (Tc a0) arising from a use of `tc'

But as Oleg already pointed out, I want to have a value `Just term ::
Maybe (Term t)' if the input is well-typed for some type which I don't
know.

Best regards,

Florian

On 09/16/2012 01:45 PM, José Pedro Magalhães wrote:
> 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
> <mailto:florian.lorenzen at tu-berlin.de>> wrote:
> 
> 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
> 
> 
> 
> 
> _______________________________________________ Haskell-Cafe
> mailing list Haskell-Cafe at haskell.org
> <mailto:Haskell-Cafe at 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 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/

iEYEARECAAYFAlBW24UACgkQvjzICpVvX7bWZACfVWRiNrJVl/ue5sk/AFsAK36m
zeUAniWoGahDymxAqkBK6JWQ5jNzDR6f
=FRcI
-----END PGP SIGNATURE-----