Received: by 10.224.117.143 with SMTP id r15mr10033046qaq.1.1349564312518;
        Sat, 06 Oct 2012 15:58:32 -0700 (PDT)
X-BeenThere: idris-lang@googlegroups.com
Received: by 10.229.135.3 with SMTP id l3ls6379749qct.6.gmail; Sat, 06 Oct
 2012 15:58:32 -0700 (PDT)
Received: by 10.224.223.84 with SMTP id ij20mr10032548qab.5.1349564312073;
        Sat, 06 Oct 2012 15:58:32 -0700 (PDT)
Received: by 10.224.223.84 with SMTP id ij20mr10032547qab.5.1349564312060;
        Sat, 06 Oct 2012 15:58:32 -0700 (PDT)
Return-Path: <ral...@gmail.com>
Received: from mail-qc0-f178.google.com (mail-qc0-f178.google.com [209.85.216.178])
        by gmr-mx.google.com with ESMTPS id f17si666225qck.1.2012.10.06.15.58.32
        (version=TLSv1/SSLv3 cipher=OTHER);
        Sat, 06 Oct 2012 15:58:32 -0700 (PDT)
Received-SPF: pass (google.com: domain of ral...@gmail.com designates 209.85.216.178 as permitted sender) client-ip=209.85.216.178;
Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of ral...@gmail.com designates 209.85.216.178 as permitted sender) smtp.mail=ral...@gmail.com; dkim=pass header...@gmail.com
Received: by mail-qc0-f178.google.com with SMTP id j34so2258069qco.37
        for <idris-lang@googlegroups.com>; Sat, 06 Oct 2012 15:58:32 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=mime-version:in-reply-to:references:date:message-id:subject:from:to
         :content-type:content-transfer-encoding;
        bh=JSuYOT6PbdBOeGgny4pUKzgp17dhYiv7uxM72sM0juM=;
        b=oFceVdDbq+9rTkn/zO25plmExlzpkILh7tlMMZ94DQ05riCER0Al1K9vrcx53UIwG1
         FlSrNZqGmHCwrZt3GHLmpfuTXJgt/juLdAjlhViMcUjwXLCMHM1xFIlVz28+DI8gLJav
         IpWqGxpjR6/mMuY5W9z/OxMmUXKzN7wlS2SuCuyi0UkdfMOWsK2o7jMH23Syr2h9iUzJ
         8J31RdddXFx5L3WHK4pyf/yp0mlEFEnPBs0SRHjV9EOLdg79WvRQEsJF3w4rKlwheNvm
         uDI/iX1Fi79XcXdAgRW+zR7FeChltRxzjmBK/RDGMylXgpzOn1jA4pkPX11EJYokI1os
         5M8A==
MIME-Version: 1.0
Received: by 10.229.38.17 with SMTP id z17mr5430993qcd.30.1349564311872; Sat,
 06 Oct 2012 15:58:31 -0700 (PDT)
Received: by 10.229.81.149 with HTTP; Sat, 6 Oct 2012 15:58:31 -0700 (PDT)
In-Reply-To: <73B49CAE-091C-459F-A237-526AECAAA...@gmail.com>
References: <73bdda7b-3490-4393-90c9-e919696900eb@googlegroups.com>
	<73B49CAE-091C-459F-A237-526AECAAA...@gmail.com>
Date: Sat, 6 Oct 2012 15:58:31 -0700
Message-ID: <CALU5TzvwiC0VUacK2zpEw84uct16cUgneDNTzy=h-ECbu4s...@mail.gmail.com>
Subject: Re: [Idris] Defunctionalization, prim__intToStr, and type safety
From: Ralith <ral...@gmail.com>
To: idris-lang@googlegroups.com
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

Is it generally true that IR case statements must handle values of
every type (by jumping to the default alternative when a type other
than that which they were written for is supplied?), or is it just
EVAL that behaves specially in that regard? The former possibility
seems counterintuitive, given how strongly typed the source language
is. Would the IR optimization passes you describe make the
aforementioned assumption completely safe again?

This brings to mind another tangental question: What motivated the
decision to use defunctionalization instead of (what I understand to
be) the more common practice of passing function pointer+environment
structs around? If it was merely the observation that not all targets
support that sort of thing, would it be reasonable for codegen for a
particular target (e.g. LLVM) to take this approach?

On Fri, Oct 5, 2012 at 5:11 AM, Edwin Brady <edwin.br...@gmail.com> wrote:
> Hi,
> If I've understood the problem correctly=E2=80=A6 the thing about EVAL is=
 that it has to be able to handle any input that is thrown at it, which cou=
ld be a primitive or a constructor, and that constructor could represent a =
function. So the C backend checks which it is first. It would be better, ev=
entually, I think, to have some compile time analysis to remove any unneces=
sary EVALs, and indeed to unbox primitives properly.
>
> One place where you might need to destructure something which turns out t=
o be an integer is where you have built a thunk to be evaluated lazily, whi=
ch will eventually turn into an integer. So it is unfortunately not a safe =
assumption that integers will never be inspected by a case - primitives can=
't assume that their inputs are fully evaluated, at least not without furth=
er compile time analysis.
>
> When I get around to it (no promises though :)) I intend to do a bit of w=
ork on the intermediate representation - specifically, a partial evaluator =
for the defunctionalised language. Some easy optimisations would be to inli=
ne primitives and do EVALs at compile time wherever possible.
>
> Edwin.