Non-productive/Non-terminating code sample
104 views
Skip to first unread message
Robert Watson
Jan 16, 2021, 4:02:40 PM1/16/21
to Idris Programming Language
This shouldn't get through the type checker (but it does for me)...something's up:
(entering 'testcode' hangs in the REPL)
booleanpred: Nat -> Bool
booleanpred Z = False
booleanpred (S k) = False
total
testList : Inf (List Nat)
testList = Z :: (map S testList)
total
testList2 : Inf (List Nat)
testList2 = filter booleanpred testList
total
oneornot : Inf (List Nat) -> Nat
oneornot xs = length (take 1 xs)
total
testcode : Nat
testcode = oneornot testList2
--oneornot testList2/ testcode
--causes problems when entered in REPL
--NON PRODUCTIVE/NON-TERMINATING CODE
--causes problems when entered in REPL
--NON PRODUCTIVE/NON-TERMINATING CODE
guillaume allais
Jan 20, 2021, 3:18:29 PM1/20/21
to Robert Watson, idris...@googlegroups.com
Oh, I see, my bad: you're using these lists as it they were
coinductive.
But they're not.
A `List` in Idris is necessarily finite unlike in Haskell for instance.
The definition of `testList` is perverse enough to trick Idris but it should
be illegal. If you want potentially infinite lists you should define a separate
type of colists in a style analogous to Stream:
defined in Prelude.Types
https://github.com/idris-lang/Idris2/blob/master/libs/prelude/Prelude/Types.idr#L388
and with library code in Data.Stream
https://github.com/idris-lang/Idris2/blob/master/libs/base/Data/Stream.idr
But they're not.
A `List` in Idris is necessarily finite unlike in Haskell for instance.
The definition of `testList` is perverse enough to trick Idris but it should
be illegal. If you want potentially infinite lists you should define a separate
type of colists in a style analogous to Stream:
defined in Prelude.Types
https://github.com/idris-lang/Idris2/blob/master/libs/prelude/Prelude/Types.idr#L388
and with library code in Data.Stream
https://github.com/idris-lang/Idris2/blob/master/libs/base/Data/Stream.idr
On 20/01/2021 17:08, Robert Watson
wrote:
Hi Guillaume,
I'm still a newbie to Idris (1 month), but I'll say how I see it...
If you change either one of the False to True then take terminates, but xs has not been fully evaluated. It can't be. If 'take' were truly strict xs should not type check because there is an 'Inf' there - it may not be possible to fully evaluate it, by definition of strict. So it may be strict up to a 'delay' or something, and that's the problem. It shouldn't type check like that. It should say "I can't prove this isn't an infinite list and as such I can't be sure to evaluate it". In other words there is a type error!
A LazyList catches the problem because a LazyList surprisingly is finite. But of course you want to be able, pragmatically and also theoretically, to apply 'take' to infinite lists (eg streams). That's crucial. BUT...how? There is a right way IMHO...
'take' should require a proof of sufficient productivity for take to terminate, where an 'external input' would suffice as a proof - I mean, waiting for input isn't quite the same as hanging! The logical responsibility for productivity passes to the external system (eg user input). A pragma based on a 'believe me' should be available to bypass that consideration so that if you aren't proving things about infinite lists you don't need to bother with any of this:
%parse inf on
If you want to have to provide a proof that 'take' will terminate (as I do!) that should require some more work. But it should be either the default, or again, activated by a pragma:
%parse inf off
or
%productivity on
...or some such.
See what I mean?
Robert
On Wed, Jan 20, 2021 at 3:03 PM guillaume allais <guillaum...@ens-lyon.org> wrote:
Hi Robert,
Isn't `take` strict in its list argument?
You may want to use the library-provided LazyList type instead of List.
Best,
On 16/01/2021 21:02, Robert Watson wrote:
CAUTION: This email originated outside the University. Check before clicking links or attachments.
--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/457d734d-519c-41cc-a779-921dae60dc4fn%40googlegroups.com.
Robert Watson
Jan 22, 2021, 9:59:48 AM1/22/21
to Idris Programming Language
Streams seem to work well, even though they use Inf in their definition. I think the problem (only my current understanding) is that Inf is unsafe, even though Streams are not (as far as I have tested their edge cases). The way I see it it matters where Inf is used in terms of future verification of Idris. The deeper the definition of Stream is placed - say for example as a builtin (just the core 'data' declaration, not the rest of the functions), the easier it might be to verify stuff later...just a thought. Inf might then be allowed or disallowed more easily via pragmas.
(The data structure I was imagining in my email to you Guillaume I now think I can easily write myself using an Either structure that captures both (finite) LazyList and (infinite) Stream.)
Robert
guillaume allais
Jan 22, 2021, 10:26:53 AM1/22/21
to idris...@googlegroups.com
Hi Robert,
I don't think you need to use `Either`. It may even give you something too strong:
you would have to, always, be able to decide in advance whether the list is finite
or not. What I was suggesting is writing a `Data.Colist` (potentially infinite lists)
library (which, btw, we'd happily merge into the standard library! ;)) by writing
code inspired by the `Data.Stream` one. Here is the type in question:
```idris
data Colist : Type -> Type where
Nil : Colist a
(::) : a -> Inf (Colist a) -> Colist a
```
This gives you both finite & infinite lists without having to decide a priori which
it is (e.g if you generate a trace corresponding to the execution of the Collatz
function, it is currently unknown whether you'd get a finite or an infinite list).
Best,
--
guillaume
I don't think you need to use `Either`. It may even give you something too strong:
you would have to, always, be able to decide in advance whether the list is finite
or not. What I was suggesting is writing a `Data.Colist` (potentially infinite lists)
library (which, btw, we'd happily merge into the standard library! ;)) by writing
code inspired by the `Data.Stream` one. Here is the type in question:
```idris
data Colist : Type -> Type where
Nil : Colist a
(::) : a -> Inf (Colist a) -> Colist a
```
This gives you both finite & infinite lists without having to decide a priori which
it is (e.g if you generate a trace corresponding to the execution of the Collatz
function, it is currently unknown whether you'd get a finite or an infinite list).
Best,
--
guillaume
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/c7799c7b-7633-47ba-811c-3bbf6fb050ban%40googlegroups.com.
Stefan Höck
Jan 22, 2021, 10:35:13 AM1/22/21
to idris...@googlegroups.com
Hi all
Sorry for jumping into this discussion. Guillaume, we already have
`Data.List.Lazy` in contrib. Could you please quickly explain
what the difference is between that one (which, if I understand
correctly, could also be potentially infinite) and your `Colist` data
type? The only difference is the use of `Inf` vs `Lazy` and I never
really understood this distinction.
Thanks
Stefan
> > <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fprelude%2FPrelude%2FTypes.idr%23L388&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C20d91dc1877b49be773e08d8bee65f8d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469243959083674%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=1iKXAKutkp%2BhMdJgdM%2F9FtDfsx6WpWwFV9Ua%2FwFQqAg%3D&reserved=0>
> > >
> > > 'take' should require a *proof *of sufficient productivity for
> > > > <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F457d734d-519c-41cc-a779-921dae60dc4fn%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C20d91dc1877b49be773e08d8bee65f8d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469243959093664%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=M7rr168TIK7c8vna1jNwGfLsAMIRdS5i3e7g3upwLZo%3D&reserved=0>.
> > To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/c7799c7b-7633-47ba-811c-3bbf6fb050ban%40googlegroups.com <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C20d91dc1877b49be773e08d8bee65f8d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469243959093664%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=SiVOiYaNr%2FCTUBnpHWv1wnaAKqzH0eu9t3epViBVGTM%3D&reserved=0>.
Sorry for jumping into this discussion. Guillaume, we already have
`Data.List.Lazy` in contrib. Could you please quickly explain
what the difference is between that one (which, if I understand
correctly, could also be potentially infinite) and your `Colist` data
type? The only difference is the use of `Inf` vs `Lazy` and I never
really understood this distinction.
Thanks
Stefan
> >
> > and with library code in Data.Stream
> > https://github.com/idris-lang/Idris2/blob/master/libs/base/Data/Stream.idr
> > <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fbase%2FData%2FStream.idr&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C20d91dc1877b49be773e08d8bee65f8d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469243959083674%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=f2n%2FuawXlt9sug42ncyBt%2BWwSjScpifnnnlKceCFAWQ%3D&reserved=0>
> > and with library code in Data.Stream
> > https://github.com/idris-lang/Idris2/blob/master/libs/base/Data/Stream.idr
> >
> > On 20/01/2021 17:08, Robert Watson wrote:
> > > Hi Guillaume,
> > >
> > > I'm still a newbie to Idris (1 month), but I'll say how I see it...
> > >
> > > If you change either one of the False to True then take
> > > terminates, but xs has not been fully evaluated. It can't be. If
> > > 'take' were truly strict xs should not type check because there
> > > is an 'Inf' there - it may not be possible to fully evaluate it,
> > > by definition of strict. So it may be strict up to a 'delay' or
> > > something, and that's the problem. It shouldn't type check like
> > > that. It should say "I can't prove this isn't an infinite list
> > > and as such I can't be sure to evaluate it". In other words there
> > > is a type error!
> > >
> > > A LazyList catches the problem because a LazyList surprisingly is
> > > finite. But of course you want to be able, pragmatically and also
> > > theoretically, to apply 'take' to infinite lists (eg streams).
> > > That's crucial. BUT...how? There _is_ a right way IMHO...
> > On 20/01/2021 17:08, Robert Watson wrote:
> > > Hi Guillaume,
> > >
> > > I'm still a newbie to Idris (1 month), but I'll say how I see it...
> > >
> > > If you change either one of the False to True then take
> > > terminates, but xs has not been fully evaluated. It can't be. If
> > > 'take' were truly strict xs should not type check because there
> > > is an 'Inf' there - it may not be possible to fully evaluate it,
> > > by definition of strict. So it may be strict up to a 'delay' or
> > > something, and that's the problem. It shouldn't type check like
> > > that. It should say "I can't prove this isn't an infinite list
> > > and as such I can't be sure to evaluate it". In other words there
> > > is a type error!
> > >
> > > A LazyList catches the problem because a LazyList surprisingly is
> > > finite. But of course you want to be able, pragmatically and also
> > > theoretically, to apply 'take' to infinite lists (eg streams).
> > >
> > > 'take' should require a *proof *of sufficient productivity for
> > >
> >
> > --
> > You received this message because you are subscribed to the Google
> > Groups "Idris Programming Language" group.
> > To unsubscribe from this group and stop receiving emails from it, send
> > an email to idris-lang+...@googlegroups.com
> > <mailto:idris-lang+...@googlegroups.com>.
> >
> > --
> > You received this message because you are subscribed to the Google
> > Groups "Idris Programming Language" group.
> > To unsubscribe from this group and stop receiving emails from it, send
> > an email to idris-lang+...@googlegroups.com
> > To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/c7799c7b-7633-47ba-811c-3bbf6fb050ban%40googlegroups.com <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C20d91dc1877b49be773e08d8bee65f8d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469243959093664%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=SiVOiYaNr%2FCTUBnpHWv1wnaAKqzH0eu9t3epViBVGTM%3D&reserved=0>.
>
> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/1f091ccd-f1c7-6eb8-41c6-349d02aa0175%40ens-lyon.org.
> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
guillaume allais
Jan 22, 2021, 11:19:00 AM1/22/21
to idris...@googlegroups.com
Hi Stefan,
I think the distinction is mostly in terms of what is used for termination checking.
If you're using `Lazy`, you are still in the inductive subset of the language (you're
just not evaluating the thunk until you actually need it). This means that the right
criterion for totality is "making a recursive call on a strict subterm". As a consequence,
```idris
eval : LazyList a -> ()
eval [] = ()
eval (_ :: xs) = eval xs
```
is total because the recursive call `eval xs` is on an argument `xs` smaller than
the input `_ :: xs`. Its effect will be to force all of the thunks in your lazylist.
On the other hand if you use `Inf`, you are now in the coinductive subset of the language
and every `Inf`-wrapped subterm may potentially be infinite. If you try to write:
```idris
eval : Colist a -> ()
eval [] = ()
eval (_ :: xs) = eval xs
```
Idris should shout at you for writing a potentially non-terminating function: for
all you know the input will be infinite and you will never in fact return `()`!
In that mode the right criterion for totality is guarded recursion. That is to say
that you are allowed to call yourself corecursively as long as this call is:
* hidden behind a constructor
* under an `Inf` barrier
i.e. instead of focusing on regularly "consuming" constructors (and thus guaranteeing
termination), you're now focusing on regularly "emitting" constructors (and thus
guaranteeing liveness).
So something like the function shouting its despair into the void:
```idris
aaaaaaa : Colist Char
aaaaaaa = 'a' :: aaaaaaa
```
is perfectly valid in the coinductive part of the language because the recursive call
is hidden behind the constructor `(::)` whose second argument is `Inf`'d. But it would
be a big no-no in the inductive one.
A classic reference to go to on these matters is Turner's Total Functional Programming.
Hope this helps,
--
guillaume
I think the distinction is mostly in terms of what is used for termination checking.
If you're using `Lazy`, you are still in the inductive subset of the language (you're
just not evaluating the thunk until you actually need it). This means that the right
criterion for totality is "making a recursive call on a strict subterm". As a consequence,
```idris
eval : LazyList a -> ()
eval [] = ()
eval (_ :: xs) = eval xs
```
is total because the recursive call `eval xs` is on an argument `xs` smaller than
the input `_ :: xs`. Its effect will be to force all of the thunks in your lazylist.
On the other hand if you use `Inf`, you are now in the coinductive subset of the language
and every `Inf`-wrapped subterm may potentially be infinite. If you try to write:
```idris
eval : Colist a -> ()
eval [] = ()
eval (_ :: xs) = eval xs
```
Idris should shout at you for writing a potentially non-terminating function: for
all you know the input will be infinite and you will never in fact return `()`!
In that mode the right criterion for totality is guarded recursion. That is to say
that you are allowed to call yourself corecursively as long as this call is:
* hidden behind a constructor
* under an `Inf` barrier
i.e. instead of focusing on regularly "consuming" constructors (and thus guaranteeing
termination), you're now focusing on regularly "emitting" constructors (and thus
guaranteeing liveness).
So something like the function shouting its despair into the void:
```idris
aaaaaaa : Colist Char
aaaaaaa = 'a' :: aaaaaaa
```
is perfectly valid in the coinductive part of the language because the recursive call
is hidden behind the constructor `(::)` whose second argument is `Inf`'d. But it would
be a big no-no in the inductive one.
A classic reference to go to on these matters is Turner's Total Functional Programming.
Hope this helps,
--
guillaume
On 22/01/2021 15:35, Stefan Höck wrote:
CAUTION: This email originated outside the University. Check before clicking links or attachments. Hi all Sorry for jumping into this discussion. Guillaume, we already have `Data.List.Lazy` in contrib. Could you please quickly explain what the difference is between that one (which, if I understand correctly, could also be potentially infinite) and your `Colist` data type? The only difference is the use of `Inf` vs `Lazy` and I never really understood this distinction. Thanks Stefan On Fri, Jan 22, 2021 at 03:26:46PM +0000, guillaume allais wrote:
Streams seem to work well, even though they use Inf in their definition. I think the problem (only my current understanding) is that Inf is unsafe, even though Streams are not (as far as I have tested their edge cases). The way I see it it matters where Inf is used in terms of future verification of Idris. The deeper the definition of Stream is placed - say for example as a builtin (just the core 'data' declaration, not the rest of the functions), the easier it might be to verify stuff later...just a thought. Inf might then be allowed or disallowed more easily via pragmas. (The data structure I was imagining in my email to you Guillaume I now think I can easily write myself using an Either structure that captures both (finite) LazyList and (infinite) Stream.) Robert On Wednesday, January 20, 2021 at 9:18:29 PM UTC+1 gallais wrote: Oh, I see, my bad: you're using these lists as it they were coinductive. But they're not. A `List` in Idris is necessarily finite unlike in Haskell for instance. The definition of `testList` is perverse enough to trick Idris but it should be illegal. If you want potentially infinite lists you should define a separate type of colists in a style analogous to Stream: defined in Prelude.Types https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fprelude%2FPrelude%2FTypes.idr%23L388&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159253428%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=JDw1vGe5A3Lpt%2Ba8jar9WBbANn5HYIi0lKlqpOp0%2BMY%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fprelude%2FPrelude%2FTypes.idr%23L388&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=NtyBLUtN2MO3X4xOEEEVT6NEPgi38K2G%2B735eZwK4oI%3D&reserved=0> and with library code in Data.Stream https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fbase%2FData%2FStream.idr&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=9s0xHR3B3qG%2BV6%2B%2Frtcsb%2F%2BrRNLXMRqUUdguh7Fdpco%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fbase%2FData%2FStream.idr&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=9s0xHR3B3qG%2BV6%2B%2Frtcsb%2F%2BrRNLXMRqUUdguh7Fdpco%3D&reserved=0>
. To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F457d734d-519c-41cc-a779-921dae60dc4fn%2540googlegroups.com&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=yoD8IpntwmuLovZT0DEoahfg%2FKm61vxipy3T0S7p3aw%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F457d734d-519c-41cc-a779-921dae60dc4fn%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=1JUVfSK3MPbLqW1XyqgnHHEY6lFBVxF5ZrXN4WAbO88%3D&reserved=0>.
-- You received this message because you are subscribed to the Google Groups "Idris Programming Language" group. To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com <mailto:idris-lang+...@googlegroups.com>
. To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=T1h9SACvMaXIsyekkzVkT0zN3W2VLJSvWbNwKFeyc6Y%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=fpbfilxBJ0O6BeA6UldLJG3fnjSEadXck6kaFsMUykU%3D&reserved=0>.
-- You received this message because you are subscribed to the Google Groups "Idris Programming Language" group. To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com
-- You received this message because you are subscribed to the Google Groups "Idris Programming Language" group. To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com
Robert Watson
Jan 23, 2021, 1:36:55 PM1/23/21
to Idris Programming Language
There's a lot there. Daily enlightenment continues with Idris!
@Stefan...I'd just add that LazyLists in Idris (unlike Haskell - or what started me off on all this which was Python generators) remain finite unless you add an Inf to them (Inf and Lazy are two very different things). If you try putting Inf in front of LazyLists similar code to what I showed above leads to the computer hanging as for Lists. And that's something I haven't been able to replicate for Streams. Presumably that also wouldn't happen for colists (?). I guess you use Inf once in the data declaration and then never use it again, as with Prelude Stream. Turner's paper can be dowloaded from the Internet.
Thanks Giullaume...I'll get on the case in a couple of weeks after I've tidied up a maths paper I just got back from review.
(Wild guess: I wonder if perhaps there ought to be a Codata declaration in Idris -dual to Data- that would avoid what seems to me to be problems with Inf?)
Robert
This shouldn't get through the type checker (but it does for me)...something's up: (entering 'testcode' hangs in the REPL) booleanpred: Nat -> Bool booleanpred Z = False booleanpred (S k) = False total testList : Inf (List Nat) testList = Z :: (map S testList) total testList2 : Inf (List Nat) testList2 = filter booleanpred testList total oneornot : Inf (List Nat) -> Nat oneornot xs = length (take 1 xs) total testcode : Nat testcode = oneornot testList2 --oneornot testList2/ testcode --causes problems when entered in REPL --NON PRODUCTIVE/NON-TERMINATING CODE -- You received this message because you are subscribed to the Google Groups "Idris Programming Language" group. To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com
. To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F457d734d-519c-41cc-a779-921dae60dc4fn%2540googlegroups.com&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=yoD8IpntwmuLovZT0DEoahfg%2FKm61vxipy3T0S7p3aw%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F457d734d-519c-41cc-a779-921dae60dc4fn%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=1JUVfSK3MPbLqW1XyqgnHHEY6lFBVxF5ZrXN4WAbO88%3D&reserved=0>.-- You received this message because you are subscribed to the Google Groups "Idris Programming Language" group. To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com <mailto:idris-lang+...@googlegroups.com>. To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=T1h9SACvMaXIsyekkzVkT0zN3W2VLJSvWbNwKFeyc6Y%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=fpbfilxBJ0O6BeA6UldLJG3fnjSEadXck6kaFsMUykU%3D&reserved=0>.
-- You received this message because you are subscribed to the Google Groups "Idris Programming Language" group. To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com-- You received this message because you are subscribed to the Google Groups "Idris Programming Language" group. To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com
Robert Watson
Feb 20, 2021, 7:35:20 AM2/20/21
to Idris Programming Language
I've basically got Colists done by the way, though I need help with Namespaces for turning it into 'style guide' library code. Will send it to Gillaume to look at soon. I came across something frustrating though: the 'where' block seems to suffer from limited functionality. Is this correct behaviour?
The following code complains about the last line in the where block,
but if I use helper function iducIndex to do the same thing instead
(and comment out the ‘where’ block) it does not. Is there a
reason for this? Or is ‘where’ not behaving as expected as I personally feel?
inducIndex : (Main.InBounds (S k) (x :: xs)) -> Main.InBounds k xs
inducIndex (InLater y) = y
||| Get the kth element of a Colist
||| @ ok proof the Colist has a kth element
public export
index : (n : Nat) -> (xs : Colist a) -> {auto ok : Main.InBounds n xs} -> a
index Z (x :: xs) = x
index (S k) (_ :: xs) {ok} = index k xs {ok = inducIndex ok}
--where
--inducIndex2 : (Main.InBounds (S k) (x :: xs)) -> Main.InBounds k xs
--inducIndex2 (InLater y) = y
Ie this does not type check:
||| Get the kth element of a Colist
||| @ ok proof the Colist has a kth element
public export
index : (n : Nat) -> (xs : Colist a) -> {auto ok : Main.InBounds n xs} -> a
index Z (x :: xs) = x
index (S k) (_ :: xs) {ok} = index k xs {ok = inducIndex2 ok}
where
inducIndex2 : (Main.InBounds (S k) (x :: xs)) -> Main.InBounds k xs
||| @ ok proof the Colist has a kth element
public export
index : (n : Nat) -> (xs : Colist a) -> {auto ok : Main.InBounds n xs} -> a
index Z (x :: xs) = x
index (S k) (_ :: xs) {ok} = index k xs {ok = inducIndex2 ok}
where
inducIndex2 : (Main.InBounds (S k) (x :: xs)) -> Main.InBounds k xs
inducIndex2 (InLater y) = y
Error(s) building file /home/robert/Code/Idris2/cRings/Dsets2.idr: While processing right hand side of index. While processing left hand side of index,inducIndex2. Can't solve constraint between: Delay ?xs and xs.
/home/robert/Code/Idris2/cRings/Dsets2.idr:248:18--248:27
|
248 | inducIndex2 (InLater y) = y
| ^^^^^^^^^
Robert
Stefan Höck
Feb 20, 2021, 11:47:53 AM2/20/21
to idris...@googlegroups.com
Hi Robert
Since you are already using `xs` in the type signature of `index`,
try using a different name in `inducIndex2` (or prefix it with a `forall xs`):
```
where
inducIndex2 : (Main.InBounds (S k) (a :: as)) -> Main.InBounds k as
The following should work also (I did not test it, though):
```
index (S k) (_ :: xs) {ok = InLater y} = index k xs {ok = y}
```
`Colist` and `Colist1` have been added to base by now, but feel free to
add additional functionality.
Stefan
> >> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fprelude%2FPrelude%2FTypes.idr%23L388&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=NtyBLUtN2MO3X4xOEEEVT6NEPgi38K2G%2B735eZwK4oI%3D&reserved=0> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fprelude%2FPrelude%2FTypes.idr%23L388&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=NtyBLUtN2MO3X4xOEEEVT6NEPgi38K2G%2B735eZwK4oI%3D&reserved=0>
> >> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fbase%2FData%2FStream.idr&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=9s0xHR3B3qG%2BV6%2B%2Frtcsb%2F%2BrRNLXMRqUUdguh7Fdpco%3D&reserved=0> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fbase%2FData%2FStream.idr&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=9s0xHR3B3qG%2BV6%2B%2Frtcsb%2F%2BrRNLXMRqUUdguh7Fdpco%3D&reserved=0>
> >> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F457d734d-519c-41cc-a779-921dae60dc4fn%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=1JUVfSK3MPbLqW1XyqgnHHEY6lFBVxF5ZrXN4WAbO88%3D&reserved=0> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F457d734d-519c-41cc-a779-921dae60dc4fn%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=1JUVfSK3MPbLqW1XyqgnHHEY6lFBVxF5ZrXN4WAbO88%3D&reserved=0>.
Since you are already using `xs` in the type signature of `index`,
try using a different name in `inducIndex2` (or prefix it with a `forall xs`):
```
where
inducIndex2 : (Main.InBounds (S k) (a :: as)) -> Main.InBounds k as
inducIndex2 (InLater y) = y
```
The following should work also (I did not test it, though):
```
public export
index : (n : Nat) -> (xs : Colist a) -> {auto ok : Main.InBounds n xs} -> a
index Z (x :: xs) {ok = _} = x
index : (n : Nat) -> (xs : Colist a) -> {auto ok : Main.InBounds n xs} -> a
index (S k) (_ :: xs) {ok = InLater y} = index k xs {ok = y}
```
`Colist` and `Colist1` have been added to base by now, but feel free to
add additional functionality.
Stefan
> >> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fbase%2FData%2FStream.idr&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=9s0xHR3B3qG%2BV6%2B%2Frtcsb%2F%2BrRNLXMRqUUdguh7Fdpco%3D&reserved=0> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fidris-lang%2FIdris2%2Fblob%2Fmaster%2Flibs%2Fbase%2FData%2FStream.idr&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=9s0xHR3B3qG%2BV6%2B%2Frtcsb%2F%2BrRNLXMRqUUdguh7Fdpco%3D&reserved=0>
> >>
> >>
> >> --
> >> You received this message because you are subscribed to the Google
> >> Groups "Idris Programming Language" group.
> >> To unsubscribe from this group and stop receiving emails from it, send
> >> an email to idris-lang+...@googlegroups.com<mailto:idris-lang+...@googlegroups.com>
> >>
> >> .
> >> To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=T1h9SACvMaXIsyekkzVkT0zN3W2VLJSvWbNwKFeyc6Y%3D&reserved=0 <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=fpbfilxBJ0O6BeA6UldLJG3fnjSEadXck6kaFsMUykU%3D&reserved=0> <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2Fc7799c7b-7633-47ba-811c-3bbf6fb050ban%2540googlegroups.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159263422%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=fpbfilxBJ0O6BeA6UldLJG3fnjSEadXck6kaFsMUykU%3D&reserved=0>.
> >>
> >> --
> >> You received this message because you are subscribed to the Google
> >> Groups "Idris Programming Language" group.
> >> To unsubscribe from this group and stop receiving emails from it, send
> >> an email to idris-lang+...@googlegroups.com<mailto:idris-lang+...@googlegroups.com>
> >>
> >> .
> >>
> >>
> >> --
> >> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> >> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com
> >>
> >> .
> >> To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F1f091ccd-f1c7-6eb8-41c6-349d02aa0175%2540ens-lyon.org&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159273416%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=LX%2FAxOvbJR1AJEDZ8seT1rCsCea%2BN0cNyJQ8x5wy%2Fls%3D&reserved=0.
> >>
> >>
> >> --
> >> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> >> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com
> >>
> >> .
> >> To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F20210122153509.GD2852%2540ruehli-laptop&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159273416%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=6OZZt1PAKrGOXl5DkkP6xq7eWWDUBshhRPSPzLPQYKM%3D&reserved=0.
> >>
> >>
> >>
>
> >>
> >> --
> >> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> >> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com
> >>
> >> .
> >> To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F1f091ccd-f1c7-6eb8-41c6-349d02aa0175%2540ens-lyon.org&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159273416%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=LX%2FAxOvbJR1AJEDZ8seT1rCsCea%2BN0cNyJQ8x5wy%2Fls%3D&reserved=0.
> >>
> >>
> >> --
> >> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> >> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com
> >>
> >> .
> >> To view this discussion on the web visit https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F20210122153509.GD2852%2540ruehli-laptop&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159273416%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=6OZZt1PAKrGOXl5DkkP6xq7eWWDUBshhRPSPzLPQYKM%3D&reserved=0.
> >>
> >>
> >>
>
> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/e9c89bb7-152b-423f-b46a-8cfd74eca416n%40googlegroups.com.
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
Robert Watson
Feb 21, 2021, 5:42:33 AM2/21/21
to Idris Programming Language
Simple enough. Thanks Stefan. I'll reinstall to get the new Base.
Here's another one I came across. The first version for lists works, the second, which looks the same but is for Colists, doesn't:
inLongerList {k = Z} {xs = (x :: xs)} (InLater prf) = InFirst
inLongerList {k = (S n)} {xs = (y :: ys)} (InLater prf) = InLater (inLongerList {k = n} {xs = ys} prf)
inLongerColist : {k : Nat} -> {xs : Colist a} -> Main.InBounds (S k) xs -> Main.InBounds k xs
inLongerColist {k = Z} {xs = (y::(Delay ys))} (InLater prf) = Main.InFirst
inLongerColist {k = (S n)} {xs = (y::(Delay ys))} (InLater prf) = Main.InLater (inLongerColist {k = n} {xs = ys} prf)
Error(s) building file /home/robert/Code/Idris2/cRings/Dsets2.idr: While processing right hand side of inLongerColist. ys is not accessible in this context.
/home/robert/Code/Idris2/cRings/Dsets2.idr:195:110--195:112
|
195 | inLongerColist {k = (S n)} {xs = (y::(Delay ys))} (InLater prf) = Main.InLater (inLongerColist {k = n} {xs = ys} prf)
| ^^
at line 195, character 110, file /home/robert/Code/Idris2/cRings/Dsets2.idr
While processing right hand side of inLongerColist. ys is not accessible in this context.
/home/robert/Code/Idris2/cRings/Dsets2.idr:195:110--195:112
|
195 | inLongerColist {k = (S n)} {xs = (y::(Delay ys))} (InLater prf) = Main.InLater (inLongerColist {k = n} {xs = ys} prf)
| ^^
Robert
Stefan Höck
Feb 21, 2021, 8:30:24 AM2/21/21
to idris...@googlegroups.com
`ys` in the line causing the issue seems to have quantity 0, though I
don't actually understand, why. The following two versions both work
(I used explicit arguments to make the whole thing a bit shorter):
```
inLongerColist : (k : Nat) -> (0 xs : Colist a) -> InBounds (S k) xs -> InBounds k xs
inLongerColist 0 _ (InLater y) = InFirst
inLongerColist (S k) (a :: Delay as) (InLater y) = InLater (inLongerColist k as y)
inLongerColist2 : (k : Nat) -> InBounds (S k) xs -> InBounds k xs
inLongerColist2 0 (InLater x) = InFirst
inLongerColist2 (S k) (InLater x) = InLater (inLongerColist2 k x)
```
However, someone else will have to explain, whether the quantity of `ys`
being 0 is expected behavior or not.
> > https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F1f091ccd-f1c7-6eb8-41c6-349d02aa0175%2540ens-lyon.org&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159273416%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=LX%2FAxOvbJR1AJEDZ8seT1rCsCea%2BN0cNyJQ8x5wy%2Fls%3D&reserved=0
don't actually understand, why. The following two versions both work
(I used explicit arguments to make the whole thing a bit shorter):
```
inLongerColist : (k : Nat) -> (0 xs : Colist a) -> InBounds (S k) xs -> InBounds k xs
inLongerColist 0 _ (InLater y) = InFirst
inLongerColist (S k) (a :: Delay as) (InLater y) = InLater (inLongerColist k as y)
inLongerColist2 : (k : Nat) -> InBounds (S k) xs -> InBounds k xs
inLongerColist2 0 (InLater x) = InFirst
inLongerColist2 (S k) (InLater x) = InLater (inLongerColist2 k x)
```
However, someone else will have to explain, whether the quantity of `ys`
being 0 is expected behavior or not.
> > .
> > > >>
> > > >>
> > > >> --
> > > >> You received this message because you are subscribed to the Google
> > Groups "Idris Programming Language" group.
> > > >> To unsubscribe from this group and stop receiving emails from it,
> > send an email to idris-lang+...@googlegroups.com
> > > >>
> > > >> .
> > > >> To view this discussion on the web visit
> > https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Fidris-lang%2F20210122153509.GD2852%2540ruehli-laptop&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C9a13f82e44ae4dbe234808d8beeb5023%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637469265159273416%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=6OZZt1PAKrGOXl5DkkP6xq7eWWDUBshhRPSPzLPQYKM%3D&reserved=0
> > > >>
> > > >>
> > > >> --
> > > >> You received this message because you are subscribed to the Google
> > Groups "Idris Programming Language" group.
> > > >> To unsubscribe from this group and stop receiving emails from it,
> > send an email to idris-lang+...@googlegroups.com
> > > >>
> > > >> .
> > > >> To view this discussion on the web visit
> > .
> > > >>
> > > >>
> > > >>
> > >
> > > --
> > > You received this message because you are subscribed to the Google
> > Groups "Idris Programming Language" group.
> > > To unsubscribe from this group and stop receiving emails from it, send
> > > >>
> > > >>
> > > >>
> > >
> > > --
> > > You received this message because you are subscribed to the Google
> > Groups "Idris Programming Language" group.
> > > To unsubscribe from this group and stop receiving emails from it, send
> > an email to idris-lang+...@googlegroups.com.
> > > To view this discussion on the web visit
> > https://groups.google.com/d/msgid/idris-lang/e9c89bb7-152b-423f-b46a-8cfd74eca416n%40googlegroups.com
> > > To view this discussion on the web visit
> > https://groups.google.com/d/msgid/idris-lang/e9c89bb7-152b-423f-b46a-8cfd74eca416n%40googlegroups.com
> > .
> >
> >
>
> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> >
> >
>
> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/c387b743-5570-4ee8-8cbe-b952ed0d819cn%40googlegroups.com.
Robert Watson
Feb 22, 2021, 11:59:13 AM2/22/21
to Idris Programming Language
As usual Idris 'works' nonetheless. But I'm curious as to why essentially the same code (with extraneous 0 xs) is tolerated by Idris in the case of Lists, but not Colists. I guess the question Is whether there's a good reason for its rejection in one case and acceptance in the other?
Robert
Robert Watson
Feb 23, 2021, 9:06:57 AM2/23/21
to Idris Programming Language
Anyway, here's some code to put inside Data.Colist.idr in base (just before 'Implementations' I guess)
It completes the functionality making Colists comparable to Lists.
I don't know if that is useful for anybody but me though!
I'll send it to Guillaume directly, and he can tell me what to do.
Comments welcome: first attempt at a contribution.
Robert
--------------------------------------------------------------------------------
-- InBounds and inBounds--------------------------------------------------------------------------------
||| Satisfiable if `k` is a valid index into `xs`
|||
||| @ k the potential index
||| @ xs the Colist into which k may be an index
public export
data InBounds : (k : Nat) -> (xs : Colist a) -> Type where
||| Z is a valid index into any cons cell
InFirst : InBounds Z (x :: (xs))
||| Valid indices can be extended
InLater : InBounds k xs -> InBounds (S k) (x :: (xs))
public export
Uninhabited (Data.Colist.InBounds k []) where
uninhabited InFirst impossible
uninhabited (InLater _) impossible
||| Decide whether `k` is a valid index into Colist `xs`
public export
inBounds : (k : Nat) -> (xs : Colist a) -> (Dec (InBounds k xs))
inBounds k xs = decCutTake (Data.List.inBounds k (take (S k) xs)) where
decCutTake: {k : Nat} -> {xs : Colist a} ->
(Dec (Data.List.InBounds (k) (take ((S k)) xs))) -> (Dec (InBounds (k) xs))
decCutTake (Yes prf) = Yes (cutTake prf) where
cutTake : {k : Nat} -> {xs : Colist a} ->
Data.List.InBounds k (Data.Colist.take (S k) xs) -> InBounds k xs
cutTake {k = Z} {xs = (y :: (Delay ys))} prf = InFirst
cutTake {k = (S x)} {xs = (y :: (Delay ys))} prf =
InLater (cutTake {k = x} (reduceColistTake (prf))) where
reduceColistTake : {xxs : Colist a} ->
Data.List.InBounds (S kk) (Data.Colist.take (S (S kk)) (xx :: (Delay xxs)))
-> Data.List.InBounds kk (Data.Colist.take (S kk) xxs)
reduceColistTake (Data.List.InLater yy) = yy
decCutTake (No contra) = No (cutTakeContra contra) where
cutTakeContra : {k : Nat} -> {xs : Colist a} ->
(Data.List.InBounds k (Data.Colist.take (S k) xs) -> Void) -> (InBounds k xs -> Void)
cutTakeContra contra bounds = contra (addTake bounds) where
addTake : {k : Nat} -> {xs : Colist a} -> Data.Colist.InBounds k xs ->
Data.List.InBounds k (Data.Colist.take (S k) xs)
addTake {k = Z} {xs = (y :: (Delay ys))} prf = InFirst
addTake {k = (S x)} {xs = (y :: (Delay ys))} prf =
InLater (addTake {k = x} (reduceColist (prf))) where
reduceColist : {xx : Nat} -> {yys : Colist a} ->
Data.Colist.InBounds (S xx) (yy :: (Delay yys)) -> Data.Colist.InBounds xx yys
reduceColist (InLater yy) = yy
guillaume allais
Feb 23, 2021, 9:19:15 AM2/23/21
to idris...@googlegroups.com
My guess is that it's due to the definition
of `InBounds`.
When you're defining an inductive type it is important to structure it so that
the return indices are simple patterns (constructors & variables) and you may
have more complex indices in the premises. There are exceptions but in general
this is what you want.
When the index is a lazy or coinductive type it's a bit trickier as Idris2 can
silently insert `Delay` and `Force` constructors. If these are inserted in the
return indices of the type, it won't be as convenient to use. So you better
declare the types of your variables to control where these are inserted.
Cf. my definition of `Any` for lazylists where I explicitly state that we have
`{0 xs : Lazy (LazyList a)}` so that the `x :: xs` in the return index really
is `x :: xs` and not `x :: Delay xs`:
https://github.com/idris-lang/Idris2/pull/1093/files#diff-9cfc0a35adfac4ec6856face94f3273901759c0c76e74976e72ee6037a85f45fR16
Without this annotation, Idris infers `{0 xs : LazyList a}` and silently inserts
a Delay in the return type which leads to confusing error messages when case
splitting on a proof of type `Any`.
Ps: if you want code to land in the libs, please open a PR on github:
https://github.com/idris-lang/Idris2/pulls.
Cheers,
--
gallais
When you're defining an inductive type it is important to structure it so that
the return indices are simple patterns (constructors & variables) and you may
have more complex indices in the premises. There are exceptions but in general
this is what you want.
When the index is a lazy or coinductive type it's a bit trickier as Idris2 can
silently insert `Delay` and `Force` constructors. If these are inserted in the
return indices of the type, it won't be as convenient to use. So you better
declare the types of your variables to control where these are inserted.
Cf. my definition of `Any` for lazylists where I explicitly state that we have
`{0 xs : Lazy (LazyList a)}` so that the `x :: xs` in the return index really
is `x :: xs` and not `x :: Delay xs`:
https://github.com/idris-lang/Idris2/pull/1093/files#diff-9cfc0a35adfac4ec6856face94f3273901759c0c76e74976e72ee6037a85f45fR16
Without this annotation, Idris infers `{0 xs : LazyList a}` and silently inserts
a Delay in the return type which leads to confusing error messages when case
splitting on a proof of type `Any`.
Ps: if you want code to land in the libs, please open a PR on github:
https://github.com/idris-lang/Idris2/pulls.
Cheers,
--
gallais
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/990291fd-c56d-4436-bb9c-3da71ea32efen%40googlegroups.com.
Robert Watson
Feb 25, 2021, 6:16:47 PM2/25/21
to Idris Programming Language
Maybe this the right idea?
data InBounds : (k : Nat) -> (xs : Colist a) -> Type where
||| Z is a valid index into any cons cell||| Valid indices can be extended
mutual
inLongerColist : {k : Nat} -> Main.InBounds (S k) xs -> Main.InBounds k xs
inLongerColist {k = Z} (InLater prf) = InFirst
inLongerColist {k = (S k)} (InLater prf) = InLonger prf
InLonger : {k : Nat} -> {0 xs : Inf (Colist a)} -> InBounds k xs -> InBounds k (x :: xs)
InLonger {k = Z} {xs} prf = InFirst
InLonger {k = (S n)} {xs} prf = InLater (inLongerColist prf)
Reply all
Reply to author
Forward
0 new messages