« First meeting of the year
Minutes »

2+2=4

I just had the following interaction with the version I just pushed:

*ParseEvalCheckRender> parseit synthit
input:
Nat => => data X : * where <z> : X ; <s> : all x : X => X
two => => <s <s <z>>> : Nat
plus => => lam m => lam n => m elim{Nat} (lam x => Nat)
% n
% (lam x => lam xh => <s xh>) :
% all m : Nat => all n : Nat => Nat
---
plus two two
STOP

<s <s <s <s <z>>>>>
data X : * where <z> : X ; <s> : all x : X => X

Some sort of progress, I think.

This entry was posted on Sunday, January 15th, 2006 at 7:22 pm and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.

5 Responses to “2+2=4”

  1. Conor Says:
    January 15th, 2006 at 8:11 pm

    Further to that, I just added a tests directory with that stuff in it. More tomorrow, but a good day’s work from the team, I think. Cheers guys!

  2. Sebastian Hanowski Says:
    January 17th, 2006 at 11:08 am

    What’s wrong with this? (I do not mean the crumbled logo)

    $ ghci -fallow-overlapping-instances ParseEvalCheckRender.lhs
    ___ ___ _
    / _ \ /\ /\/ __(_)
    / /_\// /_/ / / | | GHC Interactive, version 6.2.2, for Haskell 98.
    / /_\\/ __ / /___| | http://www.haskell.org/ghc/
    \____/\/ /_/\____/|_| Type :? for help.

    Loading package base … linking … done.
    Compiling Monoid ( ./Monoid.hs, interpreted )
    Compiling Applicative ( ./Applicative.hs, interpreted )
    Compiling Traversable ( ./Traversable.hs, interpreted )
    Compiling Idiomatics ( ./Idiomatics.lhs, interpreted )

    ./Idiomatics.lhs:202:
    Overlapping instance declarations:
    ./Idiomatics.lhs:202: AppHom Id f
    ./Idiomatics.lhs:252: AppHom a (Coprod b a)

    ./Idiomatics.lhs:214:
    Overlapping instance declarations:
    ./Idiomatics.lhs:214: AppHom g (Comp f g)
    ./Idiomatics.lhs:216: AppHom f (Comp f g)
    Failed, modules loaded: Traversable, Applicative, Monoid.
    *Traversable>

  3. pwm Says:
    January 17th, 2006 at 11:53 am

    I’d guess that your ghc version being more eager than ours, however word from Conor is that if you delete those instances for it’ll work, we don’t use the more exotic kit in the file.

    The reason your flags don’t fix it is we’ve added pragmas at the top of all our files which overrule your options and enforce ours.

  4. Sebastian Hanowski Says:
    January 18th, 2006 at 6:21 am

    It’s was due to Djinn. It’s dependency on the IntMap lib made me grab for an unstable deb archive of ghc’s.

    I didn’t understand this warning:

    /Idiomatics.lhs:214:
    Overlapping instance declarations:
    ./Idiomatics.lhs:214: AppHom g (Comp f g)
    ./Idiomatics.lhs:216: AppHom f (Comp f g)

    as these instances had already been commented out.

    And deleting instance declarations beginning at lines 202 and 252 in Idiomatics as you say evoked more overlapping-instances-warnings in Term. :(

    ./Term.lhs:212:
    Overlapping instance declarations:
    ./Term.lhs:212: Eliminable t (Bwd e)
    ./Term.lhs:227: Eliminable (Synth x) x

    ./Term.lhs:216:
    Overlapping instance declarations:
    ./Term.lhs:216: Eliminable t (Fwd e)
    ./Term.lhs:227: Eliminable (Synth x) x

    ./Term.lhs:220:
    Overlapping instance declarations:
    ./Term.lhs:220: Eliminable (Synth x) Icit
    ./Term.lhs:227: Eliminable (Synth x) x

    ./Term.lhs:224:
    Overlapping instance declarations:
    ./Term.lhs:224: Eliminable x (y, z)
    ./Term.lhs:227: Eliminable (Synth x) x

    But i can live with that for the moment. It’s just that the session log had made me curious. Thank you ☺

  5. pwm Says:
    January 18th, 2006 at 1:11 pm

    Hehe, yes well, luckily 6.4.1 only complains when it has to decide between overlapping instances and since the x in (Synth x) is never set to Bwd Fwd (,) or Icits we’re OK :)

Leave a Reply