Constraining a record type in Idris

Question

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?

TIA

Shersh Shersh · Accepted Answer · 2017-07-17T23:50:47

You can do it like this:

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

Though actually you shouldn't do it. Instead it's better to use some smart constructor, some other function like mkPoint : Eq a => a -> a -> MkPoint a. In real life you don't need to constrain types of fields for data type. Read about -XDataTypeContexts Haskell extension.

Constraining a record type in Idris

1 Answers