'parameters' blocks
36 views
Skip to first unread message
Edwin Brady
Oct 21, 2012, 7:44:57 PM10/21/12
to idris...@googlegroups.com
Hi all,
I've just added the "parameters" feature which used to exist in Idris 0.1, by request, and it'll be available from Idris 0.9.5, or in the github repository from now. It works like so:
parameters (n1 : Ty1, n2 : Ty2, …)
f : a -> b -> c
f x y = z
data Foo : a -> Set where
MkFoo : Foo a
n1, n2, etc, will be added as explicit arguments to f, Foo and MkFoo. Inside the block, they are omitted, outside the block, they must be given explicitly. Class and Instance declarations can also appear, but no parameters will be added. "parameters" blocks can be nested, and are scoped by indentation or {}s, whichever you prefer.
This is the same machinery that makes "where" clauses work. So an interesting side effect is that you can now have local data declarations if you want, such as in this contrived example, in which MyLT is only visible in the where block:
foo : Int -> Int
foo x = case isLT of
Yes => x*2
No => x*4
where
data MyLT = Yes | No
isLT : MyLT
isLT = if x < 20 then Yes else No
I have not been properly evil to this feature in testing yet (merely slightly evil), so please shout if anything doesn't work as you'd expect.
Cheers,
Edwin.
I've just added the "parameters" feature which used to exist in Idris 0.1, by request, and it'll be available from Idris 0.9.5, or in the github repository from now. It works like so:
parameters (n1 : Ty1, n2 : Ty2, …)
f : a -> b -> c
f x y = z
data Foo : a -> Set where
MkFoo : Foo a
n1, n2, etc, will be added as explicit arguments to f, Foo and MkFoo. Inside the block, they are omitted, outside the block, they must be given explicitly. Class and Instance declarations can also appear, but no parameters will be added. "parameters" blocks can be nested, and are scoped by indentation or {}s, whichever you prefer.
This is the same machinery that makes "where" clauses work. So an interesting side effect is that you can now have local data declarations if you want, such as in this contrived example, in which MyLT is only visible in the where block:
foo : Int -> Int
foo x = case isLT of
Yes => x*2
No => x*4
where
data MyLT = Yes | No
isLT : MyLT
isLT = if x < 20 then Yes else No
I have not been properly evil to this feature in testing yet (merely slightly evil), so please shout if anything doesn't work as you'd expect.
Cheers,
Edwin.
Cezar Ionescu
Oct 22, 2012, 1:45:45 AM10/22/12
to idris...@googlegroups.com, Edwin Brady
> I've just added the "parameters" feature which used to exist in Idris
> 0.1, by request, and it'll be available from Idris 0.9.5, or in the
> github repository from now.
Hurrah! Thanks, Edwin!
> 0.1, by request, and it'll be available from Idris 0.9.5, or in the
> github repository from now.
Best,
Cezar.
=================
Dr. Cezar Ionescu
Department of Transdisciplinary Concepts and Methods
Potsdam Institute for Climate Impact Research
Telegrafenberg A31
14473 Potsdam
Tel: ++49-(0)331-288-2558
Reply all
Reply to author
Forward
0 new messages