7 ms·

> the compiler can guess the implementation of the function [...] guaranteed to be correct on a type level I'm curious about this. Can you provide some example

> the compiler can guess the implementation of the function [...] guaranteed to be correct on a type level I'm curious about this. Can you provide some examples, please? Which languages can do this?

deleted 4y ago
[deleted]
adamgordonbell 4y ago
The guessing the implementation part is pretty cool. You can find videos of Edwin Brady showing it off on youtube: https://www.youtube.com/watch?v=DRq2NgeFcO0 https://www.youtube.com/watch?v=DRq2NgeFcO0 The book also walks you through lots of examples. The key part is the type needs to constrain the possible implementations down quite a bit.
jfoutz 4y ago
off the top of my head, coq agda idris. you can sort of do this with ghci and :hoogle. the simplest example is foo : A -> A since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id. another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length. All of the environments are pretty interactive, and you pick and choose. but from time to time there is exactly one possible implementation that meets all the constraints, so the compiler can fill that in.
- dunham 4y ago
  Also "Wingman" for Haskell does some type-driven code generation. (It might be part of the haskell language server now, I get it when I use the vscode plugin.) When the solution is ambiguous, Idris (and I believe wingman) will supply suggestions that you can pick from. In your `bar` case, `bar xs = 42` is also a solution. Idris suggests 0 1 2 3 ... I think, it's going off of the constructors for the return type. I expect this technology to improve over time (try to use arguments, etc.) Idris and Agda will also do stuff short of "fill in the answer" like "case split an argument for me" or "insert the appropriate constructor or lambda and leave a hole inside". This is quite helpful in cases where it's not gonna find the answer, but can type out the next step or two for you. (Wingman might have this, I haven't used it much. I don't know Coq at all.) On the Agda side, the first couple of sections of "Programming Language Foundations in Agda" will walk you through using that functionality. Idris has a couple of videos that others have pointed out. It's fun stuff.
  - jfoutz 4y ago
    in agda, I think ctrl-c ctrl-a is the "I feel lucky" button. Plfa is definitely good, Connor Mcbride is pretty good too https://www.youtube.com/playlist?list=PLqggUNm8QSqmeTg5n37oxBif-PInUfTJ2 https://www.youtube.com/playlist?list=PLqggUNm8QSqmeTg5n37ox... and yes programming with holes is almost magical. I really like "run as much as you can" then complain when you get stuck. kind of a mind blowing change for me.
  - xigoi 4y ago
    > In your `bar` case, `bar xs = 42` is also a solution. Not if you add the condition that the type must be as general as possible.
    - deleted 4y ago
      [deleted]
- JadeNB 4y ago
  > foo : A -> A > since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id. > another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length. Certainly a good suggestion, but, unlike `foo`, not the only one—e.g., `bar xs = length xs + 1` or `bar xs = 2*(length xs)` also work.
  - still_grokking 4y ago
    Maybe a better example would be `z: [A] -> [B] -> [(A, B)]`.
- Leherenn 4y ago
  While the concept is neat, I struggle a bit to see how it can be useful in practice. Do you have an example for the sufficiently constrained case? That sounds like the most interesting case by far.
  - still_grokking 4y ago
    You had a look at Hoogle? https://hoogle.haskell.org/ https://hoogle.haskell.org/ For some type signatures there is (are) only one (or only a few) meaningful implementation(s).

> the compiler can guess the implementation of the function [...] guaranteed to be correct on a type level I'm curious about this. Can you provide some examples, please? Which languages can do this?

deleted 4y ago

[deleted]

adamgordonbell 4y ago

The guessing the implementation part is pretty cool. You can find videos of Edwin Brady showing it off on youtube: https://www.youtube.com/watch?v=DRq2NgeFcO0 https://www.youtube.com/watch?v=DRq2NgeFcO0 The book also walks you through lots of examples. The key part is the type needs to constrain the possible implementations down quite a bit.

jfoutz 4y ago

off the top of my head, coq agda idris. you can sort of do this with ghci and :hoogle. the simplest example is foo : A -> A since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id. another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length. All of the environments are pretty interactive, and you pick and choose. but from time to time there is exactly one possible implementation that meets all the constraints, so the compiler can fill that in.

dunham 4y ago
Also "Wingman" for Haskell does some type-driven code generation. (It might be part of the haskell language server now, I get it when I use the vscode plugin.) When the solution is ambiguous, Idris (and I believe wingman) will supply suggestions that you can pick from. In your `bar` case, `bar xs = 42` is also a solution. Idris suggests 0 1 2 3 ... I think, it's going off of the constructors for the return type. I expect this technology to improve over time (try to use arguments, etc.) Idris and Agda will also do stuff short of "fill in the answer" like "case split an argument for me" or "insert the appropriate constructor or lambda and leave a hole inside". This is quite helpful in cases where it's not gonna find the answer, but can type out the next step or two for you. (Wingman might have this, I haven't used it much. I don't know Coq at all.) On the Agda side, the first couple of sections of "Programming Language Foundations in Agda" will walk you through using that functionality. Idris has a couple of videos that others have pointed out. It's fun stuff.
- jfoutz 4y ago
  in agda, I think ctrl-c ctrl-a is the "I feel lucky" button. Plfa is definitely good, Connor Mcbride is pretty good too https://www.youtube.com/playlist?list=PLqggUNm8QSqmeTg5n37oxBif-PInUfTJ2 https://www.youtube.com/playlist?list=PLqggUNm8QSqmeTg5n37ox... and yes programming with holes is almost magical. I really like "run as much as you can" then complain when you get stuck. kind of a mind blowing change for me.
- xigoi 4y ago
  > In your `bar` case, `bar xs = 42` is also a solution. Not if you add the condition that the type must be as general as possible.
  - deleted 4y ago
    [deleted]
JadeNB 4y ago
> foo : A -> A > since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id. > another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length. Certainly a good suggestion, but, unlike `foo`, not the only one—e.g., `bar xs = length xs + 1` or `bar xs = 2*(length xs)` also work.
- still_grokking 4y ago
  Maybe a better example would be `z: [A] -> [B] -> [(A, B)]`.
Leherenn 4y ago
While the concept is neat, I struggle a bit to see how it can be useful in practice. Do you have an example for the sufficiently constrained case? That sounds like the most interesting case by far.
- still_grokking 4y ago
  You had a look at Hoogle? https://hoogle.haskell.org/ https://hoogle.haskell.org/ For some type signatures there is (are) only one (or only a few) meaningful implementation(s).