Constraining a record type in Idris

[Rouan van Dalen]

Hi everyone,

I have asked this same question on stackoverflow, but did not get a satisfactory answer, so I thought I would ask here as well :)

I am trying to write a record in Idris but that has a generic parameter which needs to be constrained by an interface.  For normal union types I can write:

    data BSTree : (a : Type) -> Type where
      Empty : Ord a => BSTree a
      Node  : Ord a => BSTree a -> a -> BSTree a

but I am trying to figure out the syntax for doing the same thing, just with a record.  I tried something like:

    record Point a where
      constructor MkPoint : Eq a => a -> a -> Point a
      x : a
      y : a

but it does not compile.
Is there a way to do this in Idris?

I know it is possible to write something like:

    record Point a where
      constructor MkPoint
      x : Eq a => a
      y : Eq a => a

I do not want the constraint on the fields, but on the data constructor.

Regards
--Rouan

[Jan de Muijnck-Hughes]

Hi Rouan;

Thanks for asking your question.

From what I remember the syntax for records in Idris is not flexible enough to support constraints on record constructors. Unfortunately, you will have to use the long form you first presented in your email.

One approach you can consider is to use the longer form, yet hide the internal structure. Then with accessor functions, including a 'smart constructor', you can present a coherent way to create and interact with the data and ensure the constraints are presented and thus adhered to.

Jan
 

--
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.
For more options, visit https://groups.google.com/d/optout.

[Rouan van Dalen]

Hi Jan,

Thanks for the reply.  I am still new to Idris. 
Can you maybe give a code example of what you mean?

Regards
--Rouan

[G. Allais]

Hi Rouan,
What about something like this?

==========================================
module ConstrainedRecord

data EqDict : Type -> Type where
MkEqDict : Eq a => EqDict a

record Point a where
eqDict : EqDict a
x : a
y : a
==========================================

I get a warning I don't understand though:

ConstrainedRecord.idr:6:8:ConstrainedRecord.MkPoint has a name which may
be implicitly bound.
This is likely to lead to problems!

> --
> 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>.

[Rouan van Dalen]

Hi everyone,

@gallais:  Thanks for the suggestion.  

I am not really getting a satisfactory answer here,

so for the moment I am going to say that it cannot be done in a straight

forward manner and move on :)

I will maybe revisit this if there are some better alternatives to what I have seen

so far :)

Regards

--Rouan

[Jan de Muijnck-Hughes]

Rouan;

Apologies for the delay.

A simple example would be:

```idris
module Point

%access export

data Point : (a : Type) -> Type where
  MkPoint : a -> a -> Point a

newPoint : Eq a => a -> a -> Point a
newPoint = MkPoint

first : Point a -> a
first (MkPoint l _) = l

second : Point a -> a
second (MkPoint _ r) = r
```

Setting the accessor directive to `export` ensures that the constructor `MkPoint` is not exported and the only way to construct and interact with `Point a` is through the presented functions: `newPoint`, `first`, and `second`. While this is more verbose than with record functions it ensures that instances of `Point a` are created subject to the constraint on `newPoint`.

Technically, you don't need to `export` functions here. Declaring an interface constraint on `MkPoint` and using the accessors `first` and `second` is sufficient.

Hope this helps.

Jan

--

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.

[Jacob Thomas Errington]

But in this example, the instance will be forgotten as it isn't stored inside the datatype, no? Any code that consumes a Point won't be able to see the Eq instance, so what's the point?

Jake

[William ML Leslie]

On 1 August 2017 at 00:57, Jacob Thomas Errington

<ja...@mail.jerrington.me> wrote:
> But in this example, the instance will be forgotten as it isn't stored
> inside the datatype, no? Any code that consumes a Point won't be able to see
> the Eq instance, so what's the point?
>
> Jake
>

Hmm, simple test cases will work because the calling context won't
have abstracted `a`.

--
William Leslie

Notice:
Likely much of this email is, by the nature of copyright, covered
under copyright law. You absolutely MAY reproduce any part of it in
accordance with the copyright law of the nation you are reading this
in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without
prior contractual agreement.

[Rouan van Dalen]

Jan,

Thanks for the reply.

I will have a look at your example code and post here if I have more questions :)

Regards
--Rouan