So, I noticed that in Idris, if you define your own list or vector type, for example, the following type, which I found useful:
data HFVec : (f : Type -> Type) -> (n : Nat) -> Vec n Type -> Type where
Nil : HFVec f Z []
(::) : (a : f t) -> HFVec f n ts -> HFVec f (S n) (t :: ts)
- then you will get a free list syntax:
test : HFVec List 2 [Int, String]
test = [[3], [""]]
I assume this is done when you have a constructor with a name ::, but I don’t know for sure. Similarly, you get do-notation if you have a constructor with a name >>=, even if there is no monad implementation:
data Test : Type -> Type where
Pure : a -> Test a
(>>=) : Test a -> (a -> Test b) -> Test b
test : Test Int
test = do
Pure 1
x <- Pure 2
Pure x
This is a pretty cool feature, the only thing I have not found anywhere. It would be good to know how these mechanisms work, so that you can know exactly in what circumstances they can work. Also, are these rules a compiler privilege, or can they be made using functions syntaxand dsl?