-----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.loren...@tu-berlin.de
> <mailto:florian.loren...@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@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.loren...@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-----
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
